Metamath Proof Explorer


Theorem alephf1

Description: The aleph function is a one-to-one mapping from the ordinals to the infinite cardinals. See also alephf1ALT . (Contributed by Mario Carneiro, 2-Feb-2013)

Ref Expression
Assertion alephf1 ℵ : On –1-1→ On

Proof

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