Theorem domtrfil

Description: Transitivity of dominance relation when A is finite, proved without using the Axiom of Power Sets (unlike domtr ). (Contributed by BTernaryTau, 24-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		reldom	|- Rel ~<_
2	1	brrelex2i	|- ( B ~<_ C -> C e. _V )
3	2	anim2i	|- ( ( A e. Fin /\ B ~<_ C ) -> ( A e. Fin /\ C e. _V ) )
4	3	3adant2	|- ( ( A e. Fin /\ A ~<_ B /\ B ~<_ C ) -> ( A e. Fin /\ C e. _V ) )
5		brdomi	|- ( A ~<_ B -> E. g g : A -1-1-> B )
6		brdomi	|- ( B ~<_ C -> E. f f : B -1-1-> C )
7		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 ) )
8		19.42vv	|- ( E. g E. f ( ( A e. Fin /\ C e. _V ) /\ ( g : A -1-1-> B /\ f : B -1-1-> C ) ) <-> ( ( A e. Fin /\ C e. _V ) /\ E. g E. f ( g : A -1-1-> B /\ f : B -1-1-> C ) ) )
9		f1co	|- ( ( f : B -1-1-> C /\ g : A -1-1-> B ) -> ( f o. g ) : A -1-1-> C )
10	9	ancoms	|- ( ( g : A -1-1-> B /\ f : B -1-1-> C ) -> ( f o. g ) : A -1-1-> C )
11		f1domfi2	|- ( ( A e. Fin /\ C e. _V /\ ( f o. g ) : A -1-1-> C ) -> A ~<_ C )
12	11	3expa	|- ( ( ( A e. Fin /\ C e. _V ) /\ ( f o. g ) : A -1-1-> C ) -> A ~<_ C )
13	10 12	sylan2	|- ( ( ( A e. Fin /\ C e. _V ) /\ ( g : A -1-1-> B /\ f : B -1-1-> C ) ) -> A ~<_ C )
14	13	exlimivv	|- ( E. g E. f ( ( A e. Fin /\ C e. _V ) /\ ( g : A -1-1-> B /\ f : B -1-1-> C ) ) -> A ~<_ C )
15	8 14	sylbir	|- ( ( ( A e. Fin /\ C e. _V ) /\ E. g E. f ( g : A -1-1-> B /\ f : B -1-1-> C ) ) -> A ~<_ C )
16	7 15	sylan2br	|- ( ( ( A e. Fin /\ C e. _V ) /\ ( E. g g : A -1-1-> B /\ E. f f : B -1-1-> C ) ) -> A ~<_ C )
17	16	3impb	|- ( ( ( A e. Fin /\ C e. _V ) /\ E. g g : A -1-1-> B /\ E. f f : B -1-1-> C ) -> A ~<_ C )
18	6 17	syl3an3	|- ( ( ( A e. Fin /\ C e. _V ) /\ E. g g : A -1-1-> B /\ B ~<_ C ) -> A ~<_ C )
19	5 18	syl3an2	|- ( ( ( A e. Fin /\ C e. _V ) /\ A ~<_ B /\ B ~<_ C ) -> A ~<_ C )
20	4 19	syld3an1	|- ( ( A e. Fin /\ A ~<_ B /\ B ~<_ C ) -> A ~<_ C )