Step |
Hyp |
Ref |
Expression |
1 |
|
alephfnon |
⊢ ℵ Fn On |
2 |
|
isinfcard |
⊢ ( ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) ↔ 𝑥 ∈ ran ℵ ) |
3 |
2
|
bicomi |
⊢ ( 𝑥 ∈ ran ℵ ↔ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) ) |
4 |
3
|
abbi2i |
⊢ ran ℵ = { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } |
5 |
|
df-fo |
⊢ ( ℵ : On –onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ↔ ( ℵ Fn On ∧ ran ℵ = { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ) ) |
6 |
1 4 5
|
mpbir2an |
⊢ ℵ : On –onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } |
7 |
|
fof |
⊢ ( ℵ : On –onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } → ℵ : On ⟶ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ) |
8 |
6 7
|
ax-mp |
⊢ ℵ : On ⟶ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } |
9 |
|
aleph11 |
⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ( ℵ ‘ 𝑦 ) = ( ℵ ‘ 𝑧 ) ↔ 𝑦 = 𝑧 ) ) |
10 |
9
|
biimpd |
⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( ( ℵ ‘ 𝑦 ) = ( ℵ ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) |
11 |
10
|
rgen2 |
⊢ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( ( ℵ ‘ 𝑦 ) = ( ℵ ‘ 𝑧 ) → 𝑦 = 𝑧 ) |
12 |
|
dff13 |
⊢ ( ℵ : On –1-1→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ↔ ( ℵ : On ⟶ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ∧ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( ( ℵ ‘ 𝑦 ) = ( ℵ ‘ 𝑧 ) → 𝑦 = 𝑧 ) ) ) |
13 |
8 11 12
|
mpbir2an |
⊢ ℵ : On –1-1→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } |
14 |
|
df-f1o |
⊢ ( ℵ : On –1-1-onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ↔ ( ℵ : On –1-1→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ∧ ℵ : On –onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ) ) |
15 |
13 6 14
|
mpbir2an |
⊢ ℵ : On –1-1-onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } |
16 |
|
alephord2 |
⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑦 ∈ 𝑧 ↔ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑧 ) ) ) |
17 |
|
epel |
⊢ ( 𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧 ) |
18 |
|
fvex |
⊢ ( ℵ ‘ 𝑧 ) ∈ V |
19 |
18
|
epeli |
⊢ ( ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ↔ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑧 ) ) |
20 |
16 17 19
|
3bitr4g |
⊢ ( ( 𝑦 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ) ) |
21 |
20
|
rgen2 |
⊢ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ) |
22 |
|
df-isom |
⊢ ( ℵ Isom E , E ( On , { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ) ↔ ( ℵ : On –1-1-onto→ { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ∧ ∀ 𝑦 ∈ On ∀ 𝑧 ∈ On ( 𝑦 E 𝑧 ↔ ( ℵ ‘ 𝑦 ) E ( ℵ ‘ 𝑧 ) ) ) ) |
23 |
15 21 22
|
mpbir2an |
⊢ ℵ Isom E , E ( On , { 𝑥 ∣ ( ω ⊆ 𝑥 ∧ ( card ‘ 𝑥 ) = 𝑥 ) } ) |