Theorem winalim2 10610

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

Assertion

Ref	Expression
winalim2	⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))

Distinct variable group:   𝑥,𝐴

Proof of Theorem winalim2

Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		winacard 10606	. . . 4 ⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
2		winainf 10608	. . . . 5 ⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
3		cardalephex 10003	. . . . 5 ⊢ (ω ⊆ 𝐴 → ((card‘𝐴) = 𝐴 ↔ ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥)))
4	2, 3	syl 17	. . . 4 ⊢ (𝐴 ∈ Inaccw → ((card‘𝐴) = 𝐴 ↔ ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥)))
5	1, 4	mpbid 232	. . 3 ⊢ (𝐴 ∈ Inaccw → ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥))
6	5	adantr 480	. 2 ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥))
7		df-rex 3063	. . 3 ⊢ (∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥) ↔ ∃𝑥(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥)))
8		simprr 773	. . . . . . 7 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝐴 = (ℵ‘𝑥))
9	8	eqcomd 2743	. . . . . 6 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (ℵ‘𝑥) = 𝐴)
10		simprl 771	. . . . . . . 8 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝑥 ∈ On)
11		onzsl 7790	. . . . . . . 8 ⊢ (𝑥 ∈ On ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥)))
12	10, 11	sylib 218	. . . . . . 7 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥)))
13		simplr 769	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝐴 ≠ ω)
14		fveq2 6834	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (ℵ‘𝑥) = (ℵ‘∅))
15		aleph0 9979	. . . . . . . . . . . . . 14 ⊢ (ℵ‘∅) = ω
16	14, 15	eqtrdi 2788	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → (ℵ‘𝑥) = ω)
17		eqtr 2757	. . . . . . . . . . . . 13 ⊢ ((𝐴 = (ℵ‘𝑥) ∧ (ℵ‘𝑥) = ω) → 𝐴 = ω)
18	16, 17	sylan2 594	. . . . . . . . . . . 12 ⊢ ((𝐴 = (ℵ‘𝑥) ∧ 𝑥 = ∅) → 𝐴 = ω)
19	18	ex 412	. . . . . . . . . . 11 ⊢ (𝐴 = (ℵ‘𝑥) → (𝑥 = ∅ → 𝐴 = ω))
20	19	necon3ad 2946	. . . . . . . . . 10 ⊢ (𝐴 = (ℵ‘𝑥) → (𝐴 ≠ ω → ¬ 𝑥 = ∅))
21	8, 13, 20	sylc 65	. . . . . . . . 9 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ¬ 𝑥 = ∅)
22	21	pm2.21d 121	. . . . . . . 8 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (𝑥 = ∅ → Lim 𝑥))
23		breq1 5089	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (ℵ‘𝑦) → (𝑧 ≺ 𝑤 ↔ (ℵ‘𝑦) ≺ 𝑤))
24	23	rexbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑧 = (ℵ‘𝑦) → (∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 ↔ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤))
25		elwina 10600	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤))
26	25	simp3bi 1148	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Inaccw → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)
27	26	ad3antrrr 731	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)
28		onsuc 7757	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
29		vex 3434	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
30	29	sucid 6401	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ suc 𝑦
31		alephord2i 9990	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑦 ∈ On → (𝑦 ∈ suc 𝑦 → (ℵ‘𝑦) ∈ (ℵ‘suc 𝑦)))
32	28, 30, 31	mpisyl 21	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ On → (ℵ‘𝑦) ∈ (ℵ‘suc 𝑦))
33	32	ad2antrl 729	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑦) ∈ (ℵ‘suc 𝑦))
34		simplrr 778	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → 𝐴 = (ℵ‘𝑥))
35		fveq2 6834	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑦 → (ℵ‘𝑥) = (ℵ‘suc 𝑦))
36	35	ad2antll 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑥) = (ℵ‘suc 𝑦))
37	34, 36	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → 𝐴 = (ℵ‘suc 𝑦))
38	33, 37	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑦) ∈ 𝐴)
39	24, 27, 38	rspcdva 3566	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)
40	39	expr 456	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → (𝑥 = suc 𝑦 → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤))
41		iscard 9890	. . . . . . . . . . . . . . . . . . 19 ⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑤 ∈ 𝐴 𝑤 ≺ 𝐴))
42	41	simprbi 497	. . . . . . . . . . . . . . . . . 18 ⊢ ((card‘𝐴) = 𝐴 → ∀𝑤 ∈ 𝐴 𝑤 ≺ 𝐴)
43		rsp 3226	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝐴 𝑤 ≺ 𝐴 → (𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴))
44	1, 42, 43	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Inaccw → (𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴))
45	44	ad3antrrr 731	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴))
46	37	breq2d 5098	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ≺ 𝐴 ↔ 𝑤 ≺ (ℵ‘suc 𝑦)))
47	45, 46	sylibd 239	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → 𝑤 ≺ (ℵ‘suc 𝑦)))
48		alephnbtwn2 9985	. . . . . . . . . . . . . . . 16 ⊢ ¬ ((ℵ‘𝑦) ≺ 𝑤 ∧ 𝑤 ≺ (ℵ‘suc 𝑦))
49		pm3.21 471	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ≺ (ℵ‘suc 𝑦) → ((ℵ‘𝑦) ≺ 𝑤 → ((ℵ‘𝑦) ≺ 𝑤 ∧ 𝑤 ≺ (ℵ‘suc 𝑦))))
50	48, 49	mtoi 199	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ≺ (ℵ‘suc 𝑦) → ¬ (ℵ‘𝑦) ≺ 𝑤)
51	47, 50	syl6 35	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → ¬ (ℵ‘𝑦) ≺ 𝑤))
52	51	imp 406	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) ∧ 𝑤 ∈ 𝐴) → ¬ (ℵ‘𝑦) ≺ 𝑤)
53	52	nrexdv 3133	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ¬ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)
54	53	expr 456	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → (𝑥 = suc 𝑦 → ¬ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤))
55	40, 54	pm2.65d 196	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → ¬ 𝑥 = suc 𝑦)
56	55	nrexdv 3133	. . . . . . . . 9 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ¬ ∃𝑦 ∈ On 𝑥 = suc 𝑦)
57	56	pm2.21d 121	. . . . . . . 8 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (∃𝑦 ∈ On 𝑥 = suc 𝑦 → Lim 𝑥))
58		simpr 484	. . . . . . . . 9 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → Lim 𝑥)
59	58	a1i 11	. . . . . . . 8 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((𝑥 ∈ V ∧ Lim 𝑥) → Lim 𝑥))
60	22, 57, 59	3jaod 1432	. . . . . . 7 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim 𝑥))
61	12, 60	mpd 15	. . . . . 6 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → Lim 𝑥)
62	9, 61	jca 511	. . . . 5 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))
63	62	ex 412	. . . 4 ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ((𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥)) → ((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)))
64	63	eximdv 1919	. . 3 ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → (∃𝑥(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥)) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)))
65	7, 64	biimtrid 242	. 2 ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → (∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)))
66	6, 65	mpd 15	1 ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ w3o 1086   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3062  Vcvv 3430   ⊆ wss 3890  ∅c0 4274   class class class wbr 5086  Oncon0 6317  Lim wlim 6318  suc csuc 6319  ‘cfv 6492  ωcom 7810   ≺ csdm 8885  cardccrd 9850  ℵcale 9851  cfccf 9852  Inacc_wcwina 10596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-inf2 9553

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7317  df-ov 7363  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-oi 9418  df-har 9465  df-card 9854  df-aleph 9855  df-cf 9856  df-wina 10598

This theorem is referenced by:  winafp  10611