Prove more transitivity theorems for finite sets

[BTernaryTau]

Adds some additional dominance transitivity theorems for finite sets (and also renames and revises domtrfi). I realized proving transitivity when only the smallest set is finite was way easier than I initially thought, so I went back and took care of that, then used the new theorems to help prove transitivity for the strict dominance relation.

I'm not planning to add any more theorems for strict dominance or mixed relation transitivity due to the sheer number of combinations. These theorems should be enough to derive transitivity for all combinations with only a small number of additional steps.

f1domfi2

If the domain of a one-to-one function is finite, then the function's domain is dominated by its codomain when the latter is a set. This theorem is proved without using the Axiom of Power Sets (unlike ~ f1dom2g ).

domtrfil

Transitivity of dominance relation when A is finite, proved without using the Axiom of Power Sets (unlike ~ domtr ).

domtrfi

Transitivity of dominance relation when B is finite, proved without using the Axiom of Power Sets (unlike ~ domtr ).

ssdomfi2

A set dominates its finite subsets, proved without using the Axiom of Power Sets (unlike ~ ssdomg ).

domnsymfi

If a set dominates a finite set, it cannot also be strictly dominated by the finite set. This theorem is proved without using the Axiom of Power Sets (unlike ~ domnsym ).

sdomdomtrfi

Transitivity of strict dominance and dominance when A is finite, proved without using the Axiom of Power Sets (unlike ~ sdomdomtr ).

domsdomtrfi

Transitivity of dominance and strict dominance when A is finite, proved without using the Axiom of Power Sets (unlike ~ domsdomtr ).