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 ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≺ 𝐶 )

Proof

Step Hyp Ref Expression
1 sdomdom ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
2 domtrfil ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
3 1 2 syl3an2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )
4 simp1 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≈ 𝐶 ) → 𝐴 ∈ Fin )
5 ensymfib ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≈ 𝐶 ↔ 𝐶 ≈ 𝐴 ) )
6 5 biimpa ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐶 ) → 𝐶 ≈ 𝐴 )
7 6 3adant2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≈ 𝐶 ) → 𝐶 ≈ 𝐴 )
8 endom ⊢ ( 𝐶 ≈ 𝐴 → 𝐶 ≼ 𝐴 )
9 domtrfir ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐶 ≼ 𝐴 ) → 𝐵 ≼ 𝐴 )
10 8 9 syl3an3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐶 ≈ 𝐴 ) → 𝐵 ≼ 𝐴 )
11 7 10 syld3an3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≈ 𝐶 ) → 𝐵 ≼ 𝐴 )
12 domfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ Fin )
13 domnsymfi ⊢ ( ( 𝐵 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → ¬ 𝐴 ≺ 𝐵 )
14 12 13 sylancom ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ) → ¬ 𝐴 ≺ 𝐵 )
15 4 11 14 syl2anc ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≈ 𝐶 ) → ¬ 𝐴 ≺ 𝐵 )
16 15 3expia ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ) → ( 𝐴 ≈ 𝐶 → ¬ 𝐴 ≺ 𝐵 ) )
17 16 con2d ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ) → ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐶 ) )
18 17 3impia ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐶 ∧ 𝐴 ≺ 𝐵 ) → ¬ 𝐴 ≈ 𝐶 )
19 18 3com23 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → ¬ 𝐴 ≈ 𝐶 )
20 brsdom ⊢ ( 𝐴 ≺ 𝐶 ↔ ( 𝐴 ≼ 𝐶 ∧ ¬ 𝐴 ≈ 𝐶 ) )
21 3 19 20 sylanbrc ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≺ 𝐶 )