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 imbitrrdi ⊢ 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