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 |