alephval3

Description: An alternate way to express the value of the aleph function: it is the least infinite cardinal different from all values at smaller arguments. Definition of aleph in Enderton p. 212 and definition of aleph in BellMachover p. 490 . (Contributed by NM, 16-Nov-2003)

		Ref	Expression
	Assertion	alephval3	$⊢ A \in On \to ℵ (A) = ⋂ \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\}$

Proof

Step	Hyp	Ref	Expression
1		alephcard	$⊢ card (ℵ (A)) = ℵ (A)$
2	1	a1i	$⊢ A \in On \to card (ℵ (A)) = ℵ (A)$
3		alephgeom	$⊢ A \in On \leftrightarrow ω \subseteq ℵ (A)$
4	3	biimpi	$⊢ A \in On \to ω \subseteq ℵ (A)$
5		alephord2i	$⊢ A \in On \to (y \in A \to ℵ (y) \in ℵ (A))$
6		alephon	$⊢ ℵ (y) \in On$
7	6	onirri	$⊢ \neg ℵ (y) \in ℵ (y)$
8		eleq2	$⊢ ℵ (A) = ℵ (y) \to (ℵ (y) \in ℵ (A) \leftrightarrow ℵ (y) \in ℵ (y))$
9	7 8	mtbiri	$⊢ ℵ (A) = ℵ (y) \to \neg ℵ (y) \in ℵ (A)$
10	9	con2i	$⊢ ℵ (y) \in ℵ (A) \to \neg ℵ (A) = ℵ (y)$
11	5 10	syl6	$⊢ A \in On \to (y \in A \to \neg ℵ (A) = ℵ (y))$
12	11	ralrimiv	$⊢ A \in On \to \forall y \in A \neg ℵ (A) = ℵ (y)$
13		fvex	$⊢ ℵ (A) \in V$
14		fveq2	$⊢ x = ℵ (A) \to card (x) = card (ℵ (A))$
15		id	$⊢ x = ℵ (A) \to x = ℵ (A)$
16	14 15	eqeq12d	$⊢ x = ℵ (A) \to (card (x) = x \leftrightarrow card (ℵ (A)) = ℵ (A))$
17		sseq2	$⊢ x = ℵ (A) \to (ω \subseteq x \leftrightarrow ω \subseteq ℵ (A))$
18		eqeq1	$⊢ x = ℵ (A) \to (x = ℵ (y) \leftrightarrow ℵ (A) = ℵ (y))$
19	18	notbid	$⊢ x = ℵ (A) \to (\neg x = ℵ (y) \leftrightarrow \neg ℵ (A) = ℵ (y))$
20	19	ralbidv	$⊢ x = ℵ (A) \to (\forall y \in A \neg x = ℵ (y) \leftrightarrow \forall y \in A \neg ℵ (A) = ℵ (y))$
21	16 17 20	3anbi123d	$⊢ x = ℵ (A) \to ((card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y)) \leftrightarrow (card (ℵ (A)) = ℵ (A) \land ω \subseteq ℵ (A) \land \forall y \in A \neg ℵ (A) = ℵ (y)))$
22	13 21	elab	$⊢ ℵ (A) \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\} \leftrightarrow (card (ℵ (A)) = ℵ (A) \land ω \subseteq ℵ (A) \land \forall y \in A \neg ℵ (A) = ℵ (y))$
23	2 4 12 22	syl3anbrc	$⊢ A \in On \to ℵ (A) \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\}$
24		eleq1	$⊢ z = ℵ (y) \to (z \in ℵ (A) \leftrightarrow ℵ (y) \in ℵ (A))$
25		alephord2	$⊢ (y \in On \land A \in On) \to (y \in A \leftrightarrow ℵ (y) \in ℵ (A))$
26	25	bicomd	$⊢ (y \in On \land A \in On) \to (ℵ (y) \in ℵ (A) \leftrightarrow y \in A)$
27	24 26	sylan9bbr	$⊢ ((y \in On \land A \in On) \land z = ℵ (y)) \to (z \in ℵ (A) \leftrightarrow y \in A)$
28	27	biimpcd	$⊢ z \in ℵ (A) \to (((y \in On \land A \in On) \land z = ℵ (y)) \to y \in A)$
29		simpr	$⊢ ((y \in On \land A \in On) \land z = ℵ (y)) \to z = ℵ (y)$
30	28 29	jca2	$⊢ z \in ℵ (A) \to (((y \in On \land A \in On) \land z = ℵ (y)) \to (y \in A \land z = ℵ (y)))$
31	30	exp4c	$⊢ z \in ℵ (A) \to (y \in On \to (A \in On \to (z = ℵ (y) \to (y \in A \land z = ℵ (y)))))$
32	31	com3r	$⊢ A \in On \to (z \in ℵ (A) \to (y \in On \to (z = ℵ (y) \to (y \in A \land z = ℵ (y)))))$
33	32	imp4b	$⊢ (A \in On \land z \in ℵ (A)) \to ((y \in On \land z = ℵ (y)) \to (y \in A \land z = ℵ (y)))$
34	33	reximdv2	$⊢ (A \in On \land z \in ℵ (A)) \to (\exists y \in On z = ℵ (y) \to \exists y \in A z = ℵ (y))$
35		cardalephex	$⊢ ω \subseteq z \to (card (z) = z \leftrightarrow \exists y \in On z = ℵ (y))$
36	35	biimpac	$⊢ (card (z) = z \land ω \subseteq z) \to \exists y \in On z = ℵ (y)$
37	34 36	impel	$⊢ ((A \in On \land z \in ℵ (A)) \land (card (z) = z \land ω \subseteq z)) \to \exists y \in A z = ℵ (y)$
38		dfrex2	$⊢ \exists y \in A z = ℵ (y) \leftrightarrow \neg \forall y \in A \neg z = ℵ (y)$
39	37 38	sylib	$⊢ ((A \in On \land z \in ℵ (A)) \land (card (z) = z \land ω \subseteq z)) \to \neg \forall y \in A \neg z = ℵ (y)$
40		nan	$⊢ ((A \in On \land z \in ℵ (A)) \to \neg ((card (z) = z \land ω \subseteq z) \land \forall y \in A \neg z = ℵ (y))) \leftrightarrow (((A \in On \land z \in ℵ (A)) \land (card (z) = z \land ω \subseteq z)) \to \neg \forall y \in A \neg z = ℵ (y))$
41	39 40	mpbir	$⊢ (A \in On \land z \in ℵ (A)) \to \neg ((card (z) = z \land ω \subseteq z) \land \forall y \in A \neg z = ℵ (y))$
42	41	ex	$⊢ A \in On \to (z \in ℵ (A) \to \neg ((card (z) = z \land ω \subseteq z) \land \forall y \in A \neg z = ℵ (y)))$
43		vex	$⊢ z \in V$
44		fveq2	$⊢ x = z \to card (x) = card (z)$
45		id	$⊢ x = z \to x = z$
46	44 45	eqeq12d	$⊢ x = z \to (card (x) = x \leftrightarrow card (z) = z)$
47		sseq2	$⊢ x = z \to (ω \subseteq x \leftrightarrow ω \subseteq z)$
48		eqeq1	$⊢ x = z \to (x = ℵ (y) \leftrightarrow z = ℵ (y))$
49	48	notbid	$⊢ x = z \to (\neg x = ℵ (y) \leftrightarrow \neg z = ℵ (y))$
50	49	ralbidv	$⊢ x = z \to (\forall y \in A \neg x = ℵ (y) \leftrightarrow \forall y \in A \neg z = ℵ (y))$
51	46 47 50	3anbi123d	$⊢ x = z \to ((card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y)) \leftrightarrow (card (z) = z \land ω \subseteq z \land \forall y \in A \neg z = ℵ (y)))$
52	43 51	elab	$⊢ z \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\} \leftrightarrow (card (z) = z \land ω \subseteq z \land \forall y \in A \neg z = ℵ (y))$
53		df-3an	$⊢ (card (z) = z \land ω \subseteq z \land \forall y \in A \neg z = ℵ (y)) \leftrightarrow ((card (z) = z \land ω \subseteq z) \land \forall y \in A \neg z = ℵ (y))$
54	52 53	bitri	$⊢ z \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\} \leftrightarrow ((card (z) = z \land ω \subseteq z) \land \forall y \in A \neg z = ℵ (y))$
55	54	notbii	$⊢ \neg z \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\} \leftrightarrow \neg ((card (z) = z \land ω \subseteq z) \land \forall y \in A \neg z = ℵ (y))$
56	42 55	imbitrrdi	$⊢ A \in On \to (z \in ℵ (A) \to \neg z \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\})$
57	56	ralrimiv	$⊢ A \in On \to \forall z \in ℵ (A) \neg z \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\}$
58		cardon	$⊢ card (x) \in On$
59		eleq1	$⊢ card (x) = x \to (card (x) \in On \leftrightarrow x \in On)$
60	58 59	mpbii	$⊢ card (x) = x \to x \in On$
61	60	3ad2ant1	$⊢ (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y)) \to x \in On$
62	61	abssi	$⊢ \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\} \subseteq On$
63		oneqmini	$⊢ \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\} \subseteq On \to ((ℵ (A) \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\} \land \forall z \in ℵ (A) \neg z \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\}) \to ℵ (A) = ⋂ \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\})$
64	62 63	ax-mp	$⊢ (ℵ (A) \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\} \land \forall z \in ℵ (A) \neg z \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\}) \to ℵ (A) = ⋂ \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\}$
65	23 57 64	syl2anc	$⊢ A \in On \to ℵ (A) = ⋂ \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\}$

Metamath Proof Explorer

Theorem alephval3

Proof