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∈Onhar⁡A≈x→har⁡A⊆x
25 iscard2 ⊢card⁡har⁡A=har⁡A↔har⁡A∈On∧∀x∈Onhar⁡A≈x→har⁡A⊆x
26 1 24 25 mpbir2an ⊢card⁡har⁡A=har⁡A