winalim2

Description: A nontrivial weakly inaccessible cardinal is a limit aleph. (Contributed by Mario Carneiro, 29-May-2014)

		Ref	Expression
	Assertion	winalim2	$⊢ (A \in {Inacc}_{𝑤} \land A \neq ω) \to \exists x (ℵ (x) = A \land Lim x)$

Proof

Step	Hyp	Ref	Expression
1		winacard	$⊢ A \in {Inacc}_{𝑤} \to card (A) = A$
2		winainf	$⊢ A \in {Inacc}_{𝑤} \to ω \subseteq A$
3		cardalephex	$⊢ ω \subseteq A \to (card (A) = A \leftrightarrow \exists x \in On A = ℵ (x))$
4	2 3	syl	$⊢ A \in {Inacc}_{𝑤} \to (card (A) = A \leftrightarrow \exists x \in On A = ℵ (x))$
5	1 4	mpbid	$⊢ A \in {Inacc}_{𝑤} \to \exists x \in On A = ℵ (x)$
6	5	adantr	$⊢ (A \in {Inacc}_{𝑤} \land A \neq ω) \to \exists x \in On A = ℵ (x)$
7		df-rex	$⊢ \exists x \in On A = ℵ (x) \leftrightarrow \exists x (x \in On \land A = ℵ (x))$
8		simprr	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to A = ℵ (x)$
9	8	eqcomd	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to ℵ (x) = A$
10		simprl	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to x \in On$
11		onzsl	$⊢ x \in On \leftrightarrow (x = \emptyset \lor \exists y \in On x = suc y \lor (x \in V \land Lim x))$
12	10 11	sylib	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to (x = \emptyset \lor \exists y \in On x = suc y \lor (x \in V \land Lim x))$
13		simplr	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to A \neq ω$
14		fveq2	$⊢ x = \emptyset \to ℵ (x) = ℵ (\emptyset)$
15		aleph0	$⊢ ℵ (\emptyset) = ω$
16	14 15	eqtrdi	$⊢ x = \emptyset \to ℵ (x) = ω$
17		eqtr	$⊢ (A = ℵ (x) \land ℵ (x) = ω) \to A = ω$
18	16 17	sylan2	$⊢ (A = ℵ (x) \land x = \emptyset) \to A = ω$
19	18	ex	$⊢ A = ℵ (x) \to (x = \emptyset \to A = ω)$
20	19	necon3ad	$⊢ A = ℵ (x) \to (A \neq ω \to \neg x = \emptyset)$
21	8 13 20	sylc	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to \neg x = \emptyset$
22	21	pm2.21d	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to (x = \emptyset \to Lim x)$
23		breq1	$⊢ z = ℵ (y) \to (z ≺ w \leftrightarrow ℵ (y) ≺ w)$
24	23	rexbidv	$⊢ z = ℵ (y) \to (\exists w \in A z ≺ w \leftrightarrow \exists w \in A ℵ (y) ≺ w)$
25		elwina	$⊢ A \in {Inacc}_{𝑤} \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall z \in A \exists w \in A z ≺ w)$
26	25	simp3bi	$⊢ A \in {Inacc}_{𝑤} \to \forall z \in A \exists w \in A z ≺ w$
27	26	ad3antrrr	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to \forall z \in A \exists w \in A z ≺ w$
28		suceloni	$⊢ y \in On \to suc y \in On$
29		vex	$⊢ y \in V$
30	29	sucid	$⊢ y \in suc y$
31		alephord2i	$⊢ suc y \in On \to (y \in suc y \to ℵ (y) \in ℵ (suc y))$
32	28 30 31	mpisyl	$⊢ y \in On \to ℵ (y) \in ℵ (suc y)$
33	32	ad2antrl	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to ℵ (y) \in ℵ (suc y)$
34		simplrr	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to A = ℵ (x)$
35		fveq2	$⊢ x = suc y \to ℵ (x) = ℵ (suc y)$
36	35	ad2antll	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to ℵ (x) = ℵ (suc y)$
37	34 36	eqtrd	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to A = ℵ (suc y)$
38	33 37	eleqtrrd	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to ℵ (y) \in A$
39	24 27 38	rspcdva	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to \exists w \in A ℵ (y) ≺ w$
40	39	expr	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land y \in On) \to (x = suc y \to \exists w \in A ℵ (y) ≺ w)$
41		iscard	$⊢ card (A) = A \leftrightarrow (A \in On \land \forall w \in A w ≺ A)$
42	41	simprbi	$⊢ card (A) = A \to \forall w \in A w ≺ A$
43		rsp	$⊢ \forall w \in A w ≺ A \to (w \in A \to w ≺ A)$
44	1 42 43	3syl	$⊢ A \in {Inacc}_{𝑤} \to (w \in A \to w ≺ A)$
45	44	ad3antrrr	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to (w \in A \to w ≺ A)$
46	37	breq2d	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to (w ≺ A \leftrightarrow w ≺ ℵ (suc y))$
47	45 46	sylibd	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to (w \in A \to w ≺ ℵ (suc y))$
48		alephnbtwn2	$⊢ \neg (ℵ (y) ≺ w \land w ≺ ℵ (suc y))$
49		pm3.21	$⊢ w ≺ ℵ (suc y) \to (ℵ (y) ≺ w \to (ℵ (y) ≺ w \land w ≺ ℵ (suc y)))$
50	48 49	mtoi	$⊢ w ≺ ℵ (suc y) \to \neg ℵ (y) ≺ w$
51	47 50	syl6	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to (w \in A \to \neg ℵ (y) ≺ w)$
52	51	imp	$⊢ ((((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \land w \in A) \to \neg ℵ (y) ≺ w$
53	52	nrexdv	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land (y \in On \land x = suc y)) \to \neg \exists w \in A ℵ (y) ≺ w$
54	53	expr	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land y \in On) \to (x = suc y \to \neg \exists w \in A ℵ (y) ≺ w)$
55	40 54	pm2.65d	$⊢ (((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \land y \in On) \to \neg x = suc y$
56	55	nrexdv	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to \neg \exists y \in On x = suc y$
57	56	pm2.21d	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to (\exists y \in On x = suc y \to Lim x)$
58		simpr	$⊢ (x \in V \land Lim x) \to Lim x$
59	58	a1i	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to ((x \in V \land Lim x) \to Lim x)$
60	22 57 59	3jaod	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to ((x = \emptyset \lor \exists y \in On x = suc y \lor (x \in V \land Lim x)) \to Lim x)$
61	12 60	mpd	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to Lim x$
62	9 61	jca	$⊢ ((A \in {Inacc}_{𝑤} \land A \neq ω) \land (x \in On \land A = ℵ (x))) \to (ℵ (x) = A \land Lim x)$
63	62	ex	$⊢ (A \in {Inacc}_{𝑤} \land A \neq ω) \to ((x \in On \land A = ℵ (x)) \to (ℵ (x) = A \land Lim x))$
64	63	eximdv	$⊢ (A \in {Inacc}_{𝑤} \land A \neq ω) \to (\exists x (x \in On \land A = ℵ (x)) \to \exists x (ℵ (x) = A \land Lim x))$
65	7 64	syl5bi	$⊢ (A \in {Inacc}_{𝑤} \land A \neq ω) \to (\exists x \in On A = ℵ (x) \to \exists x (ℵ (x) = A \land Lim x))$
66	6 65	mpd	$⊢ (A \in {Inacc}_{𝑤} \land A \neq ω) \to \exists x (ℵ (x) = A \land Lim x)$

Metamath Proof Explorer

Theorem winalim2

Proof