Metamath Proof Explorer

Theorem fidomtri

Description: Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 27-Apr-2015)

Ref Expression
Assertion fidomtri ⊢ A ∈ Fin ∧ B ∈ V → A ≼ B ↔ ¬ B ≺ A

Proof

Step Hyp Ref Expression
1 domnsym ⊢ A ≼ B → ¬ B ≺ A
2 finnum ⊢ A ∈ Fin → A ∈ dom ⁡ card
3 2 adantr ⊢ A ∈ Fin ∧ B ∈ V → A ∈ dom ⁡ card
4 finnum ⊢ B ∈ Fin → B ∈ dom ⁡ card
5 domtri2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → A ≼ B ↔ ¬ B ≺ A
6 3 4 5 syl2an ⊢ A ∈ Fin ∧ B ∈ V ∧ B ∈ Fin → A ≼ B ↔ ¬ B ≺ A
7 6 biimprd ⊢ A ∈ Fin ∧ B ∈ V ∧ B ∈ Fin → ¬ B ≺ A → A ≼ B
8 isinffi ⊢ ¬ B ∈ Fin ∧ A ∈ Fin → ∃ a a : A ⟶ 1-1 B
9 8 ancoms ⊢ A ∈ Fin ∧ ¬ B ∈ Fin → ∃ a a : A ⟶ 1-1 B
10 9 adantlr ⊢ A ∈ Fin ∧ B ∈ V ∧ ¬ B ∈ Fin → ∃ a a : A ⟶ 1-1 B
11 brdomg ⊢ B ∈ V → A ≼ B ↔ ∃ a a : A ⟶ 1-1 B
12 11 ad2antlr ⊢ A ∈ Fin ∧ B ∈ V ∧ ¬ B ∈ Fin → A ≼ B ↔ ∃ a a : A ⟶ 1-1 B
13 10 12 mpbird ⊢ A ∈ Fin ∧ B ∈ V ∧ ¬ B ∈ Fin → A ≼ B
14 13 a1d ⊢ A ∈ Fin ∧ B ∈ V ∧ ¬ B ∈ Fin → ¬ B ≺ A → A ≼ B
15 7 14 pm2.61dan ⊢ A ∈ Fin ∧ B ∈ V → ¬ B ≺ A → A ≼ B
16 1 15 impbid2 ⊢ A ∈ Fin ∧ B ∈ V → A ≼ B ↔ ¬ B ≺ A