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

Metamath Proof Explorer

Theorem domnsymfi

Description: If a set dominates a finite set, it cannot also be strictly dominated by the finite set. This theorem is proved without using the Axiom of Power Sets (unlike domnsym ). (Contributed by BTernaryTau, 22-Nov-2024)

Ref Expression
Assertion domnsymfi ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → ¬ 𝐵 ≺ 𝐴 )

Proof

Step Hyp Ref Expression
1 brdom2 ⊢ ( 𝐴 ≼ 𝐵 ↔ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) )
2 sdomnen ⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )
3 2 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ) → ¬ 𝐴 ≈ 𝐵 )
4 sdomdom ⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
5 sdomdom ⊢ ( 𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴 )
6 sbthfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → 𝐵 ≈ 𝐴 )
7 ensymfib ⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴 ) )
8 7 3ad2ant1 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴 ) )
9 6 8 mpbird ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≈ 𝐵 )
10 5 9 syl3an2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≺ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≈ 𝐵 )
11 4 10 syl3an3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≺ 𝐴 ∧ 𝐴 ≺ 𝐵 ) → 𝐴 ≈ 𝐵 )
12 11 3com23 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐴 ) → 𝐴 ≈ 𝐵 )
13 12 3expa ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ) ∧ 𝐵 ≺ 𝐴 ) → 𝐴 ≈ 𝐵 )
14 3 13 mtand ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ) → ¬ 𝐵 ≺ 𝐴 )
15 sdomnen ⊢ ( 𝐵 ≺ 𝐴 → ¬ 𝐵 ≈ 𝐴 )
16 7 biimpa ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐵 ≈ 𝐴 )
17 15 16 nsyl3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → ¬ 𝐵 ≺ 𝐴 )
18 14 17 jaodan ⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ) → ¬ 𝐵 ≺ 𝐴 )
19 1 18 sylan2b ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → ¬ 𝐵 ≺ 𝐴 )