Metamath Proof Explorer

Theorem cardsdom2

Description: A numerable set is strictly dominated by another iff their cardinalities are strictly ordered. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion cardsdom2 ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A∈card⁡B↔A≺B

Proof

Step Hyp Ref Expression
1 carddom2 ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A⊆card⁡B↔A≼B
2 carden2 ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A=card⁡B↔A≈B
3 2 necon3abid ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A≠card⁡B↔¬A≈B
4 1 3 anbi12d ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A⊆card⁡B∧card⁡A≠card⁡B↔A≼B∧¬A≈B
5 cardon ⊢card⁡A∈On
6 cardon ⊢card⁡B∈On
7 onelpss ⊢card⁡A∈On∧card⁡B∈On→card⁡A∈card⁡B↔card⁡A⊆card⁡B∧card⁡A≠card⁡B
8 5 6 7 mp2an ⊢card⁡A∈card⁡B↔card⁡A⊆card⁡B∧card⁡A≠card⁡B
9 brsdom ⊢A≺B↔A≼B∧¬A≈B
10 4 8 9 3bitr4g ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A∈card⁡B↔A≺B