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

Metamath Proof Explorer

Theorem domsdomtrfi

Description: Transitivity of dominance and strict dominance when A is finite, proved without using the Axiom of Power Sets (unlike domsdomtr ). (Contributed by BTernaryTau, 25-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 sdomdom 
 |-  ( B ~< C -> B ~<_ C )
2 domtrfil 
 |-  ( ( A e. Fin /\ A ~<_ B /\ B ~<_ C ) -> A ~<_ C )
3 1 2 syl3an3 
 |-  ( ( A e. Fin /\ A ~<_ B /\ B ~< C ) -> A ~<_ C )
4 ensymfib 
 |-  ( A e. Fin -> ( A ~~ C <-> C ~~ A ) )
5 4 biimpa 
 |-  ( ( A e. Fin /\ A ~~ C ) -> C ~~ A )
6 5 3adant3 
 |-  ( ( A e. Fin /\ A ~~ C /\ A ~<_ B ) -> C ~~ A )
7 enfii 
 |-  ( ( A e. Fin /\ C ~~ A ) -> C e. Fin )
8 7 3adant3 
 |-  ( ( A e. Fin /\ C ~~ A /\ A ~<_ B ) -> C e. Fin )
9 endom 
 |-  ( C ~~ A -> C ~<_ A )
10 domtrfi 
 |-  ( ( A e. Fin /\ C ~<_ A /\ A ~<_ B ) -> C ~<_ B )
11 9 10 syl3an2 
 |-  ( ( A e. Fin /\ C ~~ A /\ A ~<_ B ) -> C ~<_ B )
12 8 11 jca 
 |-  ( ( A e. Fin /\ C ~~ A /\ A ~<_ B ) -> ( C e. Fin /\ C ~<_ B ) )
13 6 12 syld3an2 
 |-  ( ( A e. Fin /\ A ~~ C /\ A ~<_ B ) -> ( C e. Fin /\ C ~<_ B ) )
14 domnsymfi 
 |-  ( ( C e. Fin /\ C ~<_ B ) -> -. B ~< C )
15 13 14 syl 
 |-  ( ( A e. Fin /\ A ~~ C /\ A ~<_ B ) -> -. B ~< C )
16 15 3com23 
 |-  ( ( A e. Fin /\ A ~<_ B /\ A ~~ C ) -> -. B ~< C )
17 16 3expia 
 |-  ( ( A e. Fin /\ A ~<_ B ) -> ( A ~~ C -> -. B ~< C ) )
18 17 con2d 
 |-  ( ( A e. Fin /\ A ~<_ B ) -> ( B ~< C -> -. A ~~ C ) )
19 18 3impia 
 |-  ( ( A e. Fin /\ A ~<_ B /\ B ~< C ) -> -. A ~~ C )
20 brsdom 
 |-  ( A ~< C <-> ( A ~<_ C /\ -. A ~~ C ) )
21 3 19 20 sylanbrc 
 |-  ( ( A e. Fin /\ A ~<_ B /\ B ~< C ) -> A ~< C )