alephsmo

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

		Ref	Expression
	Assertion	alephsmo	$⊢ Smo ℵ$

Step	Hyp	Ref	Expression
1		ssid	$⊢ On \subseteq On$
2		ordon	$⊢ Ord On$
3		alephord2i	$⊢ x \in On \to (y \in x \to ℵ (y) \in ℵ (x))$
4	3	ralrimiv	$⊢ x \in On \to \forall y \in x ℵ (y) \in ℵ (x)$
5	4	rgen	$⊢ \forall x \in On \forall y \in x ℵ (y) \in ℵ (x)$
6		alephfnon	$⊢ ℵ Fn On$
7		alephsson	$⊢ ran ℵ \subseteq On$
8		df-f	$⊢ ℵ : On ⟶ On \leftrightarrow (ℵ Fn On \land ran ℵ \subseteq On)$
9	6 7 8	mpbir2an	$⊢ ℵ : On ⟶ On$
10		issmo2	$⊢ ℵ : On ⟶ On \to ((On \subseteq On \land Ord On \land \forall x \in On \forall y \in x ℵ (y) \in ℵ (x)) \to Smo ℵ)$
11	9 10	ax-mp	$⊢ (On \subseteq On \land Ord On \land \forall x \in On \forall y \in x ℵ (y) \in ℵ (x)) \to Smo ℵ$
12	1 2 5 11	mp3an	$⊢ Smo ℵ$

Metamath Proof Explorer