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

Proof

Step Hyp Ref Expression
1 sdomdom ⊢ A ≺ B → A ≼ B
2 domtrfil ⊢ A ∈ Fin ∧ A ≼ B ∧ B ≼ C → A ≼ C
3 1 2 syl3an2 ⊢ A ∈ Fin ∧ A ≺ B ∧ B ≼ C → A ≼ C
4 simp1 ⊢ A ∈ Fin ∧ B ≼ C ∧ A ≈ C → A ∈ Fin
5 ensymfib ⊢ A ∈ Fin → A ≈ C ↔ C ≈ A
6 5 biimpa ⊢ A ∈ Fin ∧ A ≈ C → C ≈ A
7 6 3adant2 ⊢ A ∈ Fin ∧ B ≼ C ∧ A ≈ C → C ≈ A
8 endom ⊢ C ≈ A → C ≼ A
9 domtrfir ⊢ A ∈ Fin ∧ B ≼ C ∧ C ≼ A → B ≼ A
10 8 9 syl3an3 ⊢ A ∈ Fin ∧ B ≼ C ∧ C ≈ A → B ≼ A
11 7 10 syld3an3 ⊢ A ∈ Fin ∧ B ≼ C ∧ A ≈ C → B ≼ A
12 domfi ⊢ A ∈ Fin ∧ B ≼ A → B ∈ Fin
13 domnsymfi ⊢ B ∈ Fin ∧ B ≼ A → ¬ A ≺ B
14 12 13 sylancom ⊢ A ∈ Fin ∧ B ≼ A → ¬ A ≺ B
15 4 11 14 syl2anc ⊢ A ∈ Fin ∧ B ≼ C ∧ A ≈ C → ¬ A ≺ B
16 15 3expia ⊢ A ∈ Fin ∧ B ≼ C → A ≈ C → ¬ A ≺ B
17 16 con2d ⊢ A ∈ Fin ∧ B ≼ C → A ≺ B → ¬ A ≈ C
18 17 3impia ⊢ A ∈ Fin ∧ B ≼ C ∧ A ≺ B → ¬ A ≈ C
19 18 3com23 ⊢ 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