Step |
Hyp |
Ref |
Expression |
1 |
|
alephfnon |
⊢ ℵ Fn On |
2 |
|
alephon |
⊢ ( ℵ ‘ 𝑥 ) ∈ On |
3 |
2
|
rgenw |
⊢ ∀ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) ∈ On |
4 |
|
ffnfv |
⊢ ( ℵ : On ⟶ On ↔ ( ℵ Fn On ∧ ∀ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) ∈ On ) ) |
5 |
1 3 4
|
mpbir2an |
⊢ ℵ : On ⟶ On |
6 |
|
aleph11 |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) ) |
7 |
6
|
biimpd |
⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) |
8 |
7
|
rgen2 |
⊢ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝑦 ) → 𝑥 = 𝑦 ) |
9 |
|
dff13 |
⊢ ( ℵ : On –1-1→ On ↔ ( ℵ : On ⟶ On ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) |
10 |
5 8 9
|
mpbir2an |
⊢ ℵ : On –1-1→ On |