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

Metamath Proof Explorer

Theorem fidomtri2

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

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

Proof

Step Hyp Ref Expression
1 domnsym ⊢ A ≼ B → ¬ B ≺ A
2 sdomdom ⊢ A ≺ B → A ≼ B
3 2 con3i ⊢ ¬ A ≼ B → ¬ A ≺ B
4 fidomtri ⊢ B ∈ Fin ∧ A ∈ V → B ≼ A ↔ ¬ A ≺ B
5 4 ancoms ⊢ A ∈ V ∧ B ∈ Fin → B ≼ A ↔ ¬ A ≺ B
6 3 5 imbitrrid ⊢ A ∈ V ∧ B ∈ Fin → ¬ A ≼ B → B ≼ A
7 ensym ⊢ B ≈ A → A ≈ B
8 endom ⊢ A ≈ B → A ≼ B
9 7 8 syl ⊢ B ≈ A → A ≼ B
10 9 con3i ⊢ ¬ A ≼ B → ¬ B ≈ A
11 6 10 jca2 ⊢ A ∈ V ∧ B ∈ Fin → ¬ A ≼ B → B ≼ A ∧ ¬ B ≈ A
12 brsdom ⊢ B ≺ A ↔ B ≼ A ∧ ¬ B ≈ A
13 11 12 imbitrrdi ⊢ A ∈ V ∧ B ∈ Fin → ¬ A ≼ B → B ≺ A
14 13 con1d ⊢ A ∈ V ∧ B ∈ Fin → ¬ B ≺ A → A ≼ B
15 1 14 impbid2 ⊢ A ∈ V ∧ B ∈ Fin → A ≼ B ↔ ¬ B ≺ A