Metamath Proof Explorer

Theorem domtri2

Description: Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion domtri2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → A ≼ B ↔ ¬ B ≺ A

Proof

Step Hyp Ref Expression
1 carddom2 ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A ⊆ card ⁡ B ↔ A ≼ B
2 cardon ⊢ card ⁡ A ∈ On
3 cardon ⊢ card ⁡ B ∈ On
4 ontri1 ⊢ card ⁡ A ∈ On ∧ card ⁡ B ∈ On → card ⁡ A ⊆ card ⁡ B ↔ ¬ card ⁡ B ∈ card ⁡ A
5 2 3 4 mp2an ⊢ card ⁡ A ⊆ card ⁡ B ↔ ¬ card ⁡ B ∈ card ⁡ A
6 cardsdom2 ⊢ B ∈ dom ⁡ card ∧ A ∈ dom ⁡ card → card ⁡ B ∈ card ⁡ A ↔ B ≺ A
7 6 ancoms ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ B ∈ card ⁡ A ↔ B ≺ A
8 7 notbid ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → ¬ card ⁡ B ∈ card ⁡ A ↔ ¬ B ≺ A
9 5 8 bitrid ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → card ⁡ A ⊆ card ⁡ B ↔ ¬ B ≺ A
10 1 9 bitr3d ⊢ A ∈ dom ⁡ card ∧ B ∈ dom ⁡ card → A ≼ B ↔ ¬ B ≺ A