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		elirr	$⊢ \neg ℵ (y) \in ℵ (y)$
7		eleq2	$⊢ ℵ (A) = ℵ (y) \to (ℵ (y) \in ℵ (A) \leftrightarrow ℵ (y) \in ℵ (y))$
8	6 7	mtbiri	$⊢ ℵ (A) = ℵ (y) \to \neg ℵ (y) \in ℵ (A)$
9	8	con2i	$⊢ ℵ (y) \in ℵ (A) \to \neg ℵ (A) = ℵ (y)$
10	5 9	syl6	$⊢ A \in On \to (y \in A \to \neg ℵ (A) = ℵ (y))$
11	10	ralrimiv	$⊢ A \in On \to \forall y \in A \neg ℵ (A) = ℵ (y)$
12		fvex	$⊢ ℵ (A) \in V$
13		fveq2	$⊢ x = ℵ (A) \to card (x) = card (ℵ (A))$
14		id	$⊢ x = ℵ (A) \to x = ℵ (A)$
15	13 14	eqeq12d	$⊢ x = ℵ (A) \to (card (x) = x \leftrightarrow card (ℵ (A)) = ℵ (A))$
16		sseq2	$⊢ x = ℵ (A) \to (ω \subseteq x \leftrightarrow ω \subseteq ℵ (A))$
17		eqeq1	$⊢ x = ℵ (A) \to (x = ℵ (y) \leftrightarrow ℵ (A) = ℵ (y))$
18	17	notbid	$⊢ x = ℵ (A) \to (\neg x = ℵ (y) \leftrightarrow \neg ℵ (A) = ℵ (y))$
19	18	ralbidv	$⊢ x = ℵ (A) \to (\forall y \in A \neg x = ℵ (y) \leftrightarrow \forall y \in A \neg ℵ (A) = ℵ (y))$
20	15 16 19	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)))$
21	12 20	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))$
22	2 4 11 21	syl3anbrc	$⊢ A \in On \to ℵ (A) \in \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\}$
23		eleq1	$⊢ z = ℵ (y) \to (z \in ℵ (A) \leftrightarrow ℵ (y) \in ℵ (A))$
24		alephord2	$⊢ (y \in On \land A \in On) \to (y \in A \leftrightarrow ℵ (y) \in ℵ (A))$
25	24	bicomd	$⊢ (y \in On \land A \in On) \to (ℵ (y) \in ℵ (A) \leftrightarrow y \in A)$
26	23 25	sylan9bbr	$⊢ ((y \in On \land A \in On) \land z = ℵ (y)) \to (z \in ℵ (A) \leftrightarrow y \in A)$
27	26	biimpcd	$⊢ z \in ℵ (A) \to (((y \in On \land A \in On) \land z = ℵ (y)) \to y \in A)$
28		simpr	$⊢ ((y \in On \land A \in On) \land z = ℵ (y)) \to z = ℵ (y)$
29	27 28	jca2	$⊢ z \in ℵ (A) \to (((y \in On \land A \in On) \land z = ℵ (y)) \to (y \in A \land z = ℵ (y)))$
30	29	exp4c	$⊢ z \in ℵ (A) \to (y \in On \to (A \in On \to (z = ℵ (y) \to (y \in A \land z = ℵ (y)))))$
31	30	com3r	$⊢ A \in On \to (z \in ℵ (A) \to (y \in On \to (z = ℵ (y) \to (y \in A \land z = ℵ (y)))))$
32	31	imp4b	$⊢ (A \in On \land z \in ℵ (A)) \to ((y \in On \land z = ℵ (y)) \to (y \in A \land z = ℵ (y)))$
33	32	reximdv2	$⊢ (A \in On \land z \in ℵ (A)) \to (\exists y \in On z = ℵ (y) \to \exists y \in A z = ℵ (y))$
34		cardalephex	$⊢ ω \subseteq z \to (card (z) = z \leftrightarrow \exists y \in On z = ℵ (y))$
35	34	biimpac	$⊢ (card (z) = z \land ω \subseteq z) \to \exists y \in On z = ℵ (y)$
36	33 35	impel	$⊢ ((A \in On \land z \in ℵ (A)) \land (card (z) = z \land ω \subseteq z)) \to \exists y \in A z = ℵ (y)$
37		dfrex2	$⊢ \exists y \in A z = ℵ (y) \leftrightarrow \neg \forall y \in A \neg z = ℵ (y)$
38	36 37	sylib	$⊢ ((A \in On \land z \in ℵ (A)) \land (card (z) = z \land ω \subseteq z)) \to \neg \forall y \in A \neg z = ℵ (y)$
39		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))$
40	38 39	mpbir	$⊢ (A \in On \land z \in ℵ (A)) \to \neg ((card (z) = z \land ω \subseteq z) \land \forall y \in A \neg z = ℵ (y))$
41	40	ex	$⊢ A \in On \to (z \in ℵ (A) \to \neg ((card (z) = z \land ω \subseteq z) \land \forall y \in A \neg z = ℵ (y)))$
42		vex	$⊢ z \in V$
43		fveq2	$⊢ x = z \to card (x) = card (z)$
44		id	$⊢ x = z \to x = z$
45	43 44	eqeq12d	$⊢ x = z \to (card (x) = x \leftrightarrow card (z) = z)$
46		sseq2	$⊢ x = z \to (ω \subseteq x \leftrightarrow ω \subseteq z)$
47		eqeq1	$⊢ x = z \to (x = ℵ (y) \leftrightarrow z = ℵ (y))$
48	47	notbid	$⊢ x = z \to (\neg x = ℵ (y) \leftrightarrow \neg z = ℵ (y))$
49	48	ralbidv	$⊢ x = z \to (\forall y \in A \neg x = ℵ (y) \leftrightarrow \forall y \in A \neg z = ℵ (y))$
50	45 46 49	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)))$
51	42 50	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))$
52		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))$
53	51 52	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))$
54	53	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))$
55	41 54	syl6ibr	$⊢ 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))\})$
56	55	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))\}$
57		cardon	$⊢ card (x) \in On$
58		eleq1	$⊢ card (x) = x \to (card (x) \in On \leftrightarrow x \in On)$
59	57 58	mpbii	$⊢ card (x) = x \to x \in On$
60	59	3ad2ant1	$⊢ (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y)) \to x \in On$
61	60	abssi	$⊢ \{x \| (card (x) = x \land ω \subseteq x \land \forall y \in A \neg x = ℵ (y))\} \subseteq On$
62		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))\})$
63	61 62	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))\}$
64	22 56 63	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