This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )