Metamath Proof Explorer

Theorem harcard

Description: The class of ordinal numbers dominated by a set is a cardinal number. Theorem 59 of Suppes p. 228. (Contributed by Mario Carneiro, 20-Jan-2013) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion harcard ⊢ card ⁡ har ⁡ A = har ⁡ A

Proof

Step Hyp Ref Expression
1 harcl ⊢ har ⁡ A ∈ On
2 harndom ⊢ ¬ har ⁡ A ≼ A
3 simpll ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → x ∈ On
4 simpr ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → y ∈ har ⁡ A
5 elharval ⊢ y ∈ har ⁡ A ↔ y ∈ On ∧ y ≼ A
6 4 5 sylib ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → y ∈ On ∧ y ≼ A
7 6 simpld ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → y ∈ On
8 ontri1 ⊢ x ∈ On ∧ y ∈ On → x ⊆ y ↔ ¬ y ∈ x
9 3 7 8 syl2anc ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → x ⊆ y ↔ ¬ y ∈ x
10 simpllr ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A ∧ x ⊆ y → har ⁡ A ≈ x
11 ssdomg ⊢ y ∈ V → x ⊆ y → x ≼ y
12 11 elv ⊢ x ⊆ y → x ≼ y
13 6 simprd ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → y ≼ A
14 domtr ⊢ x ≼ y ∧ y ≼ A → x ≼ A
15 12 13 14 syl2anr ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A ∧ x ⊆ y → x ≼ A
16 endomtr ⊢ har ⁡ A ≈ x ∧ x ≼ A → har ⁡ A ≼ A
17 10 15 16 syl2anc ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A ∧ x ⊆ y → har ⁡ A ≼ A
18 17 ex ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → x ⊆ y → har ⁡ A ≼ A
19 9 18 sylbird ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → ¬ y ∈ x → har ⁡ A ≼ A
20 2 19 mt3i ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → y ∈ x
21 20 ex ⊢ x ∈ On ∧ har ⁡ A ≈ x → y ∈ har ⁡ A → y ∈ x
22 21 ssrdv ⊢ x ∈ On ∧ har ⁡ A ≈ x → har ⁡ A ⊆ x
23 22 ex ⊢ x ∈ On → har ⁡ A ≈ x → har ⁡ A ⊆ x
24 23 rgen ⊢ ∀ x ∈ On har ⁡ A ≈ x → har ⁡ A ⊆ x
25 iscard2 ⊢ card ⁡ har ⁡ A = har ⁡ A ↔ har ⁡ A ∈ On ∧ ∀ x ∈ On har ⁡ A ≈ x → har ⁡ A ⊆ x
26 1 24 25 mpbir2an ⊢ card ⁡ har ⁡ A = har ⁡ A