alephle

Description: The argument of the aleph function is less than or equal to its value. Exercise 2 of TakeutiZaring p. 91. (Later, in alephfp2 , we will that equality can sometimes hold.) (Contributed by NM, 9-Nov-2003) (Proof shortened by Mario Carneiro, 22-Feb-2013)

		Ref	Expression
	Assertion	alephle	$⊢ A \in On \to A \subseteq ℵ (A)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ x = y \to x = y$
2		fveq2	$⊢ x = y \to ℵ (x) = ℵ (y)$
3	1 2	sseq12d	$⊢ x = y \to (x \subseteq ℵ (x) \leftrightarrow y \subseteq ℵ (y))$
4		id	$⊢ x = A \to x = A$
5		fveq2	$⊢ x = A \to ℵ (x) = ℵ (A)$
6	4 5	sseq12d	$⊢ x = A \to (x \subseteq ℵ (x) \leftrightarrow A \subseteq ℵ (A))$
7		alephord2i	$⊢ x \in On \to (y \in x \to ℵ (y) \in ℵ (x))$
8	7	imp	$⊢ (x \in On \land y \in x) \to ℵ (y) \in ℵ (x)$
9		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
10		alephon	$⊢ ℵ (x) \in On$
11		ontr2	$⊢ (y \in On \land ℵ (x) \in On) \to ((y \subseteq ℵ (y) \land ℵ (y) \in ℵ (x)) \to y \in ℵ (x))$
12	9 10 11	sylancl	$⊢ (x \in On \land y \in x) \to ((y \subseteq ℵ (y) \land ℵ (y) \in ℵ (x)) \to y \in ℵ (x))$
13	8 12	mpan2d	$⊢ (x \in On \land y \in x) \to (y \subseteq ℵ (y) \to y \in ℵ (x))$
14	13	ralimdva	$⊢ x \in On \to (\forall y \in x y \subseteq ℵ (y) \to \forall y \in x y \in ℵ (x))$
15	10	onirri	$⊢ \neg ℵ (x) \in ℵ (x)$
16		eleq1	$⊢ y = ℵ (x) \to (y \in ℵ (x) \leftrightarrow ℵ (x) \in ℵ (x))$
17	16	rspccv	$⊢ \forall y \in x y \in ℵ (x) \to (ℵ (x) \in x \to ℵ (x) \in ℵ (x))$
18	15 17	mtoi	$⊢ \forall y \in x y \in ℵ (x) \to \neg ℵ (x) \in x$
19		ontri1	$⊢ (x \in On \land ℵ (x) \in On) \to (x \subseteq ℵ (x) \leftrightarrow \neg ℵ (x) \in x)$
20	10 19	mpan2	$⊢ x \in On \to (x \subseteq ℵ (x) \leftrightarrow \neg ℵ (x) \in x)$
21	18 20	imbitrrid	$⊢ x \in On \to (\forall y \in x y \in ℵ (x) \to x \subseteq ℵ (x))$
22	14 21	syld	$⊢ x \in On \to (\forall y \in x y \subseteq ℵ (y) \to x \subseteq ℵ (x))$
23	3 6 22	tfis3	$⊢ A \in On \to A \subseteq ℵ (A)$

Metamath Proof Explorer

Theorem alephle

Proof