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