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 \underset{1-1}{⟶} On$

Proof

Step	Hyp	Ref	Expression
1		alephfnon	$⊢ ℵ Fn On$
2		alephon	$⊢ ℵ (x) \in On$
3	2	rgenw	$⊢ \forall x \in On ℵ (x) \in On$
4		ffnfv	$⊢ ℵ : On ⟶ On \leftrightarrow (ℵ Fn On \land \forall x \in On ℵ (x) \in On)$
5	1 3 4	mpbir2an	$⊢ ℵ : On ⟶ On$
6		aleph11	$⊢ (x \in On \land y \in On) \to (ℵ (x) = ℵ (y) \leftrightarrow x = y)$
7	6	biimpd	$⊢ (x \in On \land y \in On) \to (ℵ (x) = ℵ (y) \to x = y)$
8	7	rgen2	$⊢ \forall x \in On \forall y \in On (ℵ (x) = ℵ (y) \to x = y)$
9		dff13	$⊢ ℵ : On \underset{1-1}{⟶} On \leftrightarrow (ℵ : On ⟶ On \land \forall x \in On \forall y \in On (ℵ (x) = ℵ (y) \to x = y))$
10	5 8 9	mpbir2an	$⊢ ℵ : On \underset{1-1}{⟶} On$