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

Metamath Proof Explorer

Theorem alephf1ALT

Description: Alternate proof of alephf1 . (Contributed by Mario Carneiro, 15-Mar-2013) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	alephf1ALT	$⊢ ℵ : On \underset{1-1}{⟶} On$

Proof

Step	Hyp	Ref	Expression
1		alephfnon	$⊢ ℵ Fn On$
2		alephon	$⊢ ℵ (x) \in On$
3	2	a1i	$⊢ x \in On \to ℵ (x) \in On$
4	3	rgen	$⊢ \forall x \in On ℵ (x) \in On$
5		ffnfv	$⊢ ℵ : On ⟶ On \leftrightarrow (ℵ Fn On \land \forall x \in On ℵ (x) \in On)$
6	1 4 5	mpbir2an	$⊢ ℵ : On ⟶ On$
7		alephsmo	$⊢ Smo ℵ$
8		smo11	$⊢ (ℵ : On ⟶ On \land Smo ℵ) \to ℵ : On \underset{1-1}{⟶} On$
9	6 7 8	mp2an	$⊢ ℵ : On \underset{1-1}{⟶} On$