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