Theorem domtrfi

Description: Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr ). (Contributed by BTernaryTau, 17-Nov-2024)

	Ref	Expression
Assertion	domtrfi	|- ( ( C e. Fin /\ A ~<_ B /\ B ~<_ C ) -> A ~<_ C )

Proof

Step	Hyp	Ref	Expression
1		domfi	|- ( ( C e. Fin /\ B ~<_ C ) -> B e. Fin )
2		brdomg	|- ( B e. Fin -> ( A ~<_ B <-> E. g g : A -1-1-> B ) )
3	2	biimpa	|- ( ( B e. Fin /\ A ~<_ B ) -> E. g g : A -1-1-> B )
4	1 3	stoic3	|- ( ( C e. Fin /\ B ~<_ C /\ A ~<_ B ) -> E. g g : A -1-1-> B )
5	4	3com23	|- ( ( C e. Fin /\ A ~<_ B /\ B ~<_ C ) -> E. g g : A -1-1-> B )
6		brdomg	|- ( C e. Fin -> ( B ~<_ C <-> E. f f : B -1-1-> C ) )
7	6	biimpa	|- ( ( C e. Fin /\ B ~<_ C ) -> E. f f : B -1-1-> C )
8	7	3adant2	|- ( ( C e. Fin /\ E. g g : A -1-1-> B /\ B ~<_ C ) -> E. f f : B -1-1-> C )
9		exdistrv	|- ( E. g E. f ( g : A -1-1-> B /\ f : B -1-1-> C ) <-> ( E. g g : A -1-1-> B /\ E. f f : B -1-1-> C ) )
10		19.42vv	|- ( E. g E. f ( C e. Fin /\ ( g : A -1-1-> B /\ f : B -1-1-> C ) ) <-> ( C e. Fin /\ E. g E. f ( g : A -1-1-> B /\ f : B -1-1-> C ) ) )
11		f1co	|- ( ( f : B -1-1-> C /\ g : A -1-1-> B ) -> ( f o. g ) : A -1-1-> C )
12	11	ancoms	|- ( ( g : A -1-1-> B /\ f : B -1-1-> C ) -> ( f o. g ) : A -1-1-> C )
13		f1domfi	|- ( ( C e. Fin /\ ( f o. g ) : A -1-1-> C ) -> A ~<_ C )
14	12 13	sylan2	|- ( ( C e. Fin /\ ( g : A -1-1-> B /\ f : B -1-1-> C ) ) -> A ~<_ C )
15	14	exlimivv	|- ( E. g E. f ( C e. Fin /\ ( g : A -1-1-> B /\ f : B -1-1-> C ) ) -> A ~<_ C )
16	10 15	sylbir	|- ( ( C e. Fin /\ E. g E. f ( g : A -1-1-> B /\ f : B -1-1-> C ) ) -> A ~<_ C )
17	9 16	sylan2br	|- ( ( C e. Fin /\ ( E. g g : A -1-1-> B /\ E. f f : B -1-1-> C ) ) -> A ~<_ C )
18	17	3impb	|- ( ( C e. Fin /\ E. g g : A -1-1-> B /\ E. f f : B -1-1-> C ) -> A ~<_ C )
19	8 18	syld3an3	|- ( ( C e. Fin /\ E. g g : A -1-1-> B /\ B ~<_ C ) -> A ~<_ C )
20	5 19	syld3an2	|- ( ( C e. Fin /\ A ~<_ B /\ B ~<_ C ) -> A ~<_ C )