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

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

Proof

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