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 |
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 |