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

Proof

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