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

Metamath Proof Explorer

Theorem sdomdomtrfi

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

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

Proof

Step Hyp Ref Expression
1 sdomdom 
 |-  ( A ~< B -> A ~<_ B )
2 domtrfil 
 |-  ( ( A e. Fin /\ A ~<_ B /\ B ~<_ C ) -> A ~<_ C )
3 1 2 syl3an2 
 |-  ( ( A e. Fin /\ A ~< B /\ B ~<_ C ) -> A ~<_ C )
4 simp1 
 |-  ( ( A e. Fin /\ B ~<_ C /\ A ~~ C ) -> A e. Fin )
5 ensymfib 
 |-  ( A e. Fin -> ( A ~~ C <-> C ~~ A ) )
6 5 biimpa 
 |-  ( ( A e. Fin /\ A ~~ C ) -> C ~~ A )
7 6 3adant2 
 |-  ( ( A e. Fin /\ B ~<_ C /\ A ~~ C ) -> C ~~ A )
8 endom 
 |-  ( C ~~ A -> C ~<_ A )
9 domtrfir 
 |-  ( ( A e. Fin /\ B ~<_ C /\ C ~<_ A ) -> B ~<_ A )
10 8 9 syl3an3 
 |-  ( ( A e. Fin /\ B ~<_ C /\ C ~~ A ) -> B ~<_ A )
11 7 10 syld3an3 
 |-  ( ( A e. Fin /\ B ~<_ C /\ A ~~ C ) -> B ~<_ A )
12 domfi 
 |-  ( ( A e. Fin /\ B ~<_ A ) -> B e. Fin )
13 domnsymfi 
 |-  ( ( B e. Fin /\ B ~<_ A ) -> -. A ~< B )
14 12 13 sylancom 
 |-  ( ( A e. Fin /\ B ~<_ A ) -> -. A ~< B )
15 4 11 14 syl2anc 
 |-  ( ( A e. Fin /\ B ~<_ C /\ A ~~ C ) -> -. A ~< B )
16 15 3expia 
 |-  ( ( A e. Fin /\ B ~<_ C ) -> ( A ~~ C -> -. A ~< B ) )
17 16 con2d 
 |-  ( ( A e. Fin /\ B ~<_ C ) -> ( A ~< B -> -. A ~~ C ) )
18 17 3impia 
 |-  ( ( A e. Fin /\ B ~<_ C /\ A ~< B ) -> -. A ~~ C )
19 18 3com23 
 |-  ( ( 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 )