This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℵ