Theorem alephsmo

Description: The aleph function is strictly monotone. (Contributed by Mario Carneiro, 15-Mar-2013)

	Ref	Expression
Assertion	alephsmo	⊢ Smo ℵ

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ On ⊆ On
2		ordon	⊢ Ord On
3		alephord2i	⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) ) )
4	3	ralrimiv	⊢ ( 𝑥 ∈ On → ∀ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) )
5	4	rgen	⊢ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 )
6		alephfnon	⊢ ℵ Fn On
7		alephsson	⊢ ran ℵ ⊆ On
8		df-f	⊢ ( ℵ : On ⟶ On ↔ ( ℵ Fn On ∧ ran ℵ ⊆ On ) )
9	6 7 8	mpbir2an	⊢ ℵ : On ⟶ On
10		issmo2	⊢ ( ℵ : On ⟶ On → ( ( On ⊆ On ∧ Ord On ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) ) → Smo ℵ ) )
11	9 10	ax-mp	⊢ ( ( On ⊆ On ∧ Ord On ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ 𝑥 ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) ) → Smo ℵ )
12	1 2 5 11	mp3an	⊢ Smo ℵ