This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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