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