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

Proof

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