Step |
Hyp |
Ref |
Expression |
1 |
|
alephsuc2 |
⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } ) |
2 |
|
alephcard |
⊢ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) |
3 |
|
alephon |
⊢ ( ℵ ‘ 𝐴 ) ∈ On |
4 |
|
onenon |
⊢ ( ( ℵ ‘ 𝐴 ) ∈ On → ( ℵ ‘ 𝐴 ) ∈ dom card ) |
5 |
3 4
|
ax-mp |
⊢ ( ℵ ‘ 𝐴 ) ∈ dom card |
6 |
|
cardval2 |
⊢ ( ( ℵ ‘ 𝐴 ) ∈ dom card → ( card ‘ ( ℵ ‘ 𝐴 ) ) = { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } ) |
7 |
5 6
|
ax-mp |
⊢ ( card ‘ ( ℵ ‘ 𝐴 ) ) = { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } |
8 |
2 7
|
eqtr3i |
⊢ ( ℵ ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } |
9 |
8
|
a1i |
⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) = { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } ) |
10 |
1 9
|
difeq12d |
⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ suc 𝐴 ) ∖ ( ℵ ‘ 𝐴 ) ) = ( { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } ∖ { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } ) ) |
11 |
|
difrab |
⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } ∖ { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } ) = { 𝑥 ∈ On ∣ ( 𝑥 ≼ ( ℵ ‘ 𝐴 ) ∧ ¬ 𝑥 ≺ ( ℵ ‘ 𝐴 ) ) } |
12 |
|
bren2 |
⊢ ( 𝑥 ≈ ( ℵ ‘ 𝐴 ) ↔ ( 𝑥 ≼ ( ℵ ‘ 𝐴 ) ∧ ¬ 𝑥 ≺ ( ℵ ‘ 𝐴 ) ) ) |
13 |
12
|
rabbii |
⊢ { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } = { 𝑥 ∈ On ∣ ( 𝑥 ≼ ( ℵ ‘ 𝐴 ) ∧ ¬ 𝑥 ≺ ( ℵ ‘ 𝐴 ) ) } |
14 |
11 13
|
eqtr4i |
⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≼ ( ℵ ‘ 𝐴 ) } ∖ { 𝑥 ∈ On ∣ 𝑥 ≺ ( ℵ ‘ 𝐴 ) } ) = { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } |
15 |
10 14
|
eqtr2di |
⊢ ( 𝐴 ∈ On → { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } = ( ( ℵ ‘ suc 𝐴 ) ∖ ( ℵ ‘ 𝐴 ) ) ) |
16 |
|
alephon |
⊢ ( ℵ ‘ suc 𝐴 ) ∈ On |
17 |
|
onenon |
⊢ ( ( ℵ ‘ suc 𝐴 ) ∈ On → ( ℵ ‘ suc 𝐴 ) ∈ dom card ) |
18 |
16 17
|
mp1i |
⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) ∈ dom card ) |
19 |
|
sucelon |
⊢ ( 𝐴 ∈ On ↔ suc 𝐴 ∈ On ) |
20 |
|
alephgeom |
⊢ ( suc 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ suc 𝐴 ) ) |
21 |
19 20
|
bitri |
⊢ ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ suc 𝐴 ) ) |
22 |
|
fvex |
⊢ ( ℵ ‘ suc 𝐴 ) ∈ V |
23 |
|
ssdomg |
⊢ ( ( ℵ ‘ suc 𝐴 ) ∈ V → ( ω ⊆ ( ℵ ‘ suc 𝐴 ) → ω ≼ ( ℵ ‘ suc 𝐴 ) ) ) |
24 |
22 23
|
ax-mp |
⊢ ( ω ⊆ ( ℵ ‘ suc 𝐴 ) → ω ≼ ( ℵ ‘ suc 𝐴 ) ) |
25 |
21 24
|
sylbi |
⊢ ( 𝐴 ∈ On → ω ≼ ( ℵ ‘ suc 𝐴 ) ) |
26 |
|
alephordilem1 |
⊢ ( 𝐴 ∈ On → ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 ) ) |
27 |
|
infdif |
⊢ ( ( ( ℵ ‘ suc 𝐴 ) ∈ dom card ∧ ω ≼ ( ℵ ‘ suc 𝐴 ) ∧ ( ℵ ‘ 𝐴 ) ≺ ( ℵ ‘ suc 𝐴 ) ) → ( ( ℵ ‘ suc 𝐴 ) ∖ ( ℵ ‘ 𝐴 ) ) ≈ ( ℵ ‘ suc 𝐴 ) ) |
28 |
18 25 26 27
|
syl3anc |
⊢ ( 𝐴 ∈ On → ( ( ℵ ‘ suc 𝐴 ) ∖ ( ℵ ‘ 𝐴 ) ) ≈ ( ℵ ‘ suc 𝐴 ) ) |
29 |
15 28
|
eqbrtrd |
⊢ ( 𝐴 ∈ On → { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } ≈ ( ℵ ‘ suc 𝐴 ) ) |
30 |
29
|
ensymd |
⊢ ( 𝐴 ∈ On → ( ℵ ‘ suc 𝐴 ) ≈ { 𝑥 ∈ On ∣ 𝑥 ≈ ( ℵ ‘ 𝐴 ) } ) |