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∈Fin∧A≼B∧B≺C→A≺C

Proof

Step Hyp Ref Expression
1 sdomdom ⊢B≺C→B≼C
2 domtrfil ⊢A∈Fin∧A≼B∧B≼C→A≼C
3 1 2 syl3an3 ⊢A∈Fin∧A≼B∧B≺C→A≼C
4 ensymfib ⊢A∈Fin→A≈C↔C≈A
5 4 biimpa ⊢A∈Fin∧A≈C→C≈A
6 5 3adant3 ⊢A∈Fin∧A≈C∧A≼B→C≈A
7 enfii ⊢A∈Fin∧C≈A→C∈Fin
8 7 3adant3 ⊢A∈Fin∧C≈A∧A≼B→C∈Fin
9 endom ⊢C≈A→C≼A
10 domtrfi ⊢A∈Fin∧C≼A∧A≼B→C≼B
11 9 10 syl3an2 ⊢A∈Fin∧C≈A∧A≼B→C≼B
12 8 11 jca ⊢A∈Fin∧C≈A∧A≼B→C∈Fin∧C≼B
13 6 12 syld3an2 ⊢A∈Fin∧A≈C∧A≼B→C∈Fin∧C≼B
14 domnsymfi ⊢C∈Fin∧C≼B→¬B≺C
15 13 14 syl ⊢A∈Fin∧A≈C∧A≼B→¬B≺C
16 15 3com23 ⊢A∈Fin∧A≼B∧A≈C→¬B≺C
17 16 3expia ⊢A∈Fin∧A≼B→A≈C→¬B≺C
18 17 con2d ⊢A∈Fin∧A≼B→B≺C→¬A≈C
19 18 3impia ⊢A∈Fin∧A≼B∧B≺C→¬A≈C
20 brsdom ⊢A≺C↔A≼C∧¬A≈C
21 3 19 20 sylanbrc ⊢A∈Fin∧A≼B∧B≺C→A≺C