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 ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ 𝑉 ) → ( ( card ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) → 𝐴 ≼ 𝐵 ) )

Proof

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