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 ‘ 𝐴 ) ) = ( har ‘ 𝐴 )

Proof

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