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