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 ⊢ x ∈ On → y ∈ x → ℵ ⁡ y ∈ ℵ ⁡ x
4 3 ralrimiv ⊢ x ∈ On → ∀ y ∈ x ℵ ⁡ y ∈ ℵ ⁡ x
5 4 rgen ⊢ ∀ x ∈ On ∀ y ∈ x ℵ ⁡ y ∈ ℵ ⁡ x
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 ∧ ∀ x ∈ On ∀ y ∈ x ℵ ⁡ y ∈ ℵ ⁡ x → Smo ⁡ ℵ
11 9 10 ax-mp ⊢ On ⊆ On ∧ Ord ⁡ On ∧ ∀ x ∈ On ∀ y ∈ x ℵ ⁡ y ∈ ℵ ⁡ x → Smo ⁡ ℵ
12 1 2 5 11 mp3an ⊢ Smo ⁡ ℵ