This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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