Metamath Proof Explorer

Theorem carddomi2

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

Ref Expression
Assertion carddomi2 ⊢A∈dom⁡card∧B∈V→card⁡A⊆card⁡B→A≼B

Proof

Step Hyp Ref Expression
1 cardnueq0 ⊢A∈dom⁡card→card⁡A=∅↔A=∅
2 1 adantr ⊢A∈dom⁡card∧B∈V→card⁡A=∅↔A=∅
3 2 biimpa ⊢A∈dom⁡card∧B∈V∧card⁡A=∅→A=∅
4 0domg ⊢B∈V→∅≼B
5 4 ad2antlr ⊢A∈dom⁡card∧B∈V∧card⁡A=∅→∅≼B
6 3 5 eqbrtrd ⊢A∈dom⁡card∧B∈V∧card⁡A=∅→A≼B
7 6 a1d ⊢A∈dom⁡card∧B∈V∧card⁡A=∅→card⁡A⊆card⁡B→A≼B
8 fvex ⊢card⁡B∈V
9 simprr ⊢A∈dom⁡card∧B∈V∧card⁡A≠∅∧card⁡A⊆card⁡B→card⁡A⊆card⁡B
10 ssdomg ⊢card⁡B∈V→card⁡A⊆card⁡B→card⁡A≼card⁡B
11 8 9 10 mpsyl ⊢A∈dom⁡card∧B∈V∧card⁡A≠∅∧card⁡A⊆card⁡B→card⁡A≼card⁡B
12 cardid2 ⊢A∈dom⁡card→card⁡A≈A
13 12 ad2antrr ⊢A∈dom⁡card∧B∈V∧card⁡A≠∅∧card⁡A⊆card⁡B→card⁡A≈A
14 simprl ⊢A∈dom⁡card∧B∈V∧card⁡A≠∅∧card⁡A⊆card⁡B→card⁡A≠∅
15 ssn0 ⊢card⁡A⊆card⁡B∧card⁡A≠∅→card⁡B≠∅
16 9 14 15 syl2anc ⊢A∈dom⁡card∧B∈V∧card⁡A≠∅∧card⁡A⊆card⁡B→card⁡B≠∅
17 ndmfv ⊢¬B∈dom⁡card→card⁡B=∅
18 17 necon1ai ⊢card⁡B≠∅→B∈dom⁡card
19 cardid2 ⊢B∈dom⁡card→card⁡B≈B
20 16 18 19 3syl ⊢A∈dom⁡card∧B∈V∧card⁡A≠∅∧card⁡A⊆card⁡B→card⁡B≈B
21 domen1 ⊢card⁡A≈A→card⁡A≼card⁡B↔A≼card⁡B
22 domen2 ⊢card⁡B≈B→A≼card⁡B↔A≼B
23 21 22 sylan9bb ⊢card⁡A≈A∧card⁡B≈B→card⁡A≼card⁡B↔A≼B
24 13 20 23 syl2anc ⊢A∈dom⁡card∧B∈V∧card⁡A≠∅∧card⁡A⊆card⁡B→card⁡A≼card⁡B↔A≼B
25 11 24 mpbid ⊢A∈dom⁡card∧B∈V∧card⁡A≠∅∧card⁡A⊆card⁡B→A≼B
26 25 expr ⊢A∈dom⁡card∧B∈V∧card⁡A≠∅→card⁡A⊆card⁡B→A≼B
27 7 26 pm2.61dane ⊢A∈dom⁡card∧B∈V→card⁡A⊆card⁡B→A≼B