Metamath Proof Explorer

Theorem carddom2

Description: Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom , which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion carddom2 ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A⊆card⁡B↔A≼B

Proof

Step Hyp Ref Expression
1 carddomi2 ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A⊆card⁡B→A≼B
2 brdom2 ⊢A≼B↔A≺B∨A≈B
3 cardon ⊢card⁡A∈On
4 3 onelssi ⊢card⁡B∈card⁡A→card⁡B⊆card⁡A
5 carddomi2 ⊢B∈dom⁡card∧A∈dom⁡card→card⁡B⊆card⁡A→B≼A
6 5 ancoms ⊢A∈dom⁡card∧B∈dom⁡card→card⁡B⊆card⁡A→B≼A
7 domnsym ⊢B≼A→¬A≺B
8 4 6 7 syl56 ⊢A∈dom⁡card∧B∈dom⁡card→card⁡B∈card⁡A→¬A≺B
9 8 con2d ⊢A∈dom⁡card∧B∈dom⁡card→A≺B→¬card⁡B∈card⁡A
10 cardon ⊢card⁡B∈On
11 ontri1 ⊢card⁡A∈On∧card⁡B∈On→card⁡A⊆card⁡B↔¬card⁡B∈card⁡A
12 3 10 11 mp2an ⊢card⁡A⊆card⁡B↔¬card⁡B∈card⁡A
13 9 12 syl6ibr ⊢A∈dom⁡card∧B∈dom⁡card→A≺B→card⁡A⊆card⁡B
14 carden2b ⊢A≈B→card⁡A=card⁡B
15 eqimss ⊢card⁡A=card⁡B→card⁡A⊆card⁡B
16 14 15 syl ⊢A≈B→card⁡A⊆card⁡B
17 16 a1i ⊢A∈dom⁡card∧B∈dom⁡card→A≈B→card⁡A⊆card⁡B
18 13 17 jaod ⊢A∈dom⁡card∧B∈dom⁡card→A≺B∨A≈B→card⁡A⊆card⁡B
19 2 18 biimtrid ⊢A∈dom⁡card∧B∈dom⁡card→A≼B→card⁡A⊆card⁡B
20 1 19 impbid ⊢A∈dom⁡card∧B∈dom⁡card→card⁡A⊆card⁡B↔A≼B