| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cardidm |
⊢ ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) |
| 2 |
|
cardom |
⊢ ( card ‘ ω ) = ω |
| 3 |
|
simpr |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ω ≼ 𝐴 ) |
| 4 |
|
omelon |
⊢ ω ∈ On |
| 5 |
|
onenon |
⊢ ( ω ∈ On → ω ∈ dom card ) |
| 6 |
4 5
|
ax-mp |
⊢ ω ∈ dom card |
| 7 |
|
simpl |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → 𝐴 ∈ dom card ) |
| 8 |
|
carddom2 |
⊢ ( ( ω ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ( card ‘ ω ) ⊆ ( card ‘ 𝐴 ) ↔ ω ≼ 𝐴 ) ) |
| 9 |
6 7 8
|
sylancr |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ( card ‘ ω ) ⊆ ( card ‘ 𝐴 ) ↔ ω ≼ 𝐴 ) ) |
| 10 |
3 9
|
mpbird |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( card ‘ ω ) ⊆ ( card ‘ 𝐴 ) ) |
| 11 |
2 10
|
eqsstrrid |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ω ⊆ ( card ‘ 𝐴 ) ) |
| 12 |
|
cardalephex |
⊢ ( ω ⊆ ( card ‘ 𝐴 ) → ( ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) ↔ ∃ 𝑥 ∈ On ( card ‘ 𝐴 ) = ( ℵ ‘ 𝑥 ) ) ) |
| 13 |
11 12
|
syl |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ( card ‘ ( card ‘ 𝐴 ) ) = ( card ‘ 𝐴 ) ↔ ∃ 𝑥 ∈ On ( card ‘ 𝐴 ) = ( ℵ ‘ 𝑥 ) ) ) |
| 14 |
1 13
|
mpbii |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ∃ 𝑥 ∈ On ( card ‘ 𝐴 ) = ( ℵ ‘ 𝑥 ) ) |
| 15 |
|
eqcom |
⊢ ( ( card ‘ 𝐴 ) = ( ℵ ‘ 𝑥 ) ↔ ( ℵ ‘ 𝑥 ) = ( card ‘ 𝐴 ) ) |
| 16 |
15
|
rexbii |
⊢ ( ∃ 𝑥 ∈ On ( card ‘ 𝐴 ) = ( ℵ ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ 𝐴 ) ) |
| 17 |
14 16
|
sylib |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ 𝐴 ) ) |
| 18 |
|
alephfnon |
⊢ ℵ Fn On |
| 19 |
|
fvelrnb |
⊢ ( ℵ Fn On → ( ( card ‘ 𝐴 ) ∈ ran ℵ ↔ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ 𝐴 ) ) ) |
| 20 |
18 19
|
ax-mp |
⊢ ( ( card ‘ 𝐴 ) ∈ ran ℵ ↔ ∃ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) = ( card ‘ 𝐴 ) ) |
| 21 |
17 20
|
sylibr |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( card ‘ 𝐴 ) ∈ ran ℵ ) |
| 22 |
|
cardid2 |
⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 ) |
| 23 |
22
|
adantr |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( card ‘ 𝐴 ) ≈ 𝐴 ) |
| 24 |
|
breq1 |
⊢ ( 𝑥 = ( card ‘ 𝐴 ) → ( 𝑥 ≈ 𝐴 ↔ ( card ‘ 𝐴 ) ≈ 𝐴 ) ) |
| 25 |
24
|
rspcev |
⊢ ( ( ( card ‘ 𝐴 ) ∈ ran ℵ ∧ ( card ‘ 𝐴 ) ≈ 𝐴 ) → ∃ 𝑥 ∈ ran ℵ 𝑥 ≈ 𝐴 ) |
| 26 |
21 23 25
|
syl2anc |
⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ∃ 𝑥 ∈ ran ℵ 𝑥 ≈ 𝐴 ) |