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 elharval ⊢ y ∈ har ⁡ A ↔ y ∈ On ∧ y ≼ A
5 4 bilani ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → y ∈ On ∧ y ≼ A
6 5 simpld ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → y ∈ On
7 ontri1 ⊢ x ∈ On ∧ y ∈ On → x ⊆ y ↔ ¬ y ∈ x
8 3 6 7 syl2anc ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → x ⊆ y ↔ ¬ y ∈ x
9 simpllr ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A ∧ x ⊆ y → har ⁡ A ≈ x
10 ssdomg ⊢ y ∈ V → x ⊆ y → x ≼ y
11 10 elv ⊢ x ⊆ y → x ≼ y
12 5 simprd ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → y ≼ A
13 domtr ⊢ x ≼ y ∧ y ≼ A → x ≼ A
14 11 12 13 syl2anr ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A ∧ x ⊆ y → x ≼ A
15 endomtr ⊢ har ⁡ A ≈ x ∧ x ≼ A → har ⁡ A ≼ A
16 9 14 15 syl2anc ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A ∧ x ⊆ y → har ⁡ A ≼ A
17 16 ex ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → x ⊆ y → har ⁡ A ≼ A
18 8 17 sylbird ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → ¬ y ∈ x → har ⁡ A ≼ A
19 2 18 mt3i ⊢ x ∈ On ∧ har ⁡ A ≈ x ∧ y ∈ har ⁡ A → y ∈ x
20 19 ex ⊢ x ∈ On ∧ har ⁡ A ≈ x → y ∈ har ⁡ A → y ∈ x
21 20 ssrdv ⊢ x ∈ On ∧ har ⁡ A ≈ x → har ⁡ A ⊆ x
22 21 ex ⊢ x ∈ On → har ⁡ A ≈ x → har ⁡ A ⊆ x
23 22 rgen ⊢ ∀ x ∈ On har ⁡ A ≈ x → har ⁡ A ⊆ x
24 iscard2 ⊢ card ⁡ har ⁡ A = har ⁡ A ↔ har ⁡ A ∈ On ∧ ∀ x ∈ On har ⁡ A ≈ x → har ⁡ A ⊆ x
25 1 23 24 mpbir2an ⊢ card ⁡ har ⁡ A = har ⁡ A