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 –1-1→ On

Proof

Step Hyp Ref Expression
1 alephfnon ℵ Fn On
2 alephon ( ℵ ‘ 𝑥 ) ∈ On
3 2 a1i ( 𝑥 ∈ On → ( ℵ ‘ 𝑥 ) ∈ On )
4 3 rgen 𝑥 ∈ On ( ℵ ‘ 𝑥 ) ∈ On
5 ffnfv ( ℵ : On ⟶ On ↔ ( ℵ Fn On ∧ ∀ 𝑥 ∈ On ( ℵ ‘ 𝑥 ) ∈ On ) )
6 1 4 5 mpbir2an ℵ : On ⟶ On
7 alephsmo Smo ℵ
8 smo11 ( ( ℵ : On ⟶ On ∧ Smo ℵ ) → ℵ : On –1-1→ On )
9 6 7 8 mp2an ℵ : On –1-1→ On