Theorem winalim2 10619

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 10615	. . . 4 ⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
2		winainf 10617	. . . . 5 ⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
3		cardalephex 10012	. . . . 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 7798	. . . . . . . 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 6842	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (ℵ‘𝑥) = (ℵ‘∅))
15		aleph0 9988	. . . . . . . . . . . . . 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 5103	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (ℵ‘𝑦) → (𝑧 ≺ 𝑤 ↔ (ℵ‘𝑦) ≺ 𝑤))
24	23	rexbidv 3162	. . . . . . . . . . . . 13 ⊢ (𝑧 = (ℵ‘𝑦) → (∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 ↔ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤))
25		elwina 10609	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤))
26	25	simp3bi 1148	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Inaccw → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)
27	26	ad3antrrr 731	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)
28		onsuc 7765	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
29		vex 3446	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
30	29	sucid 6409	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ suc 𝑦
31		alephord2i 9999	. . . . . . . . . . . . . . . 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 6842	. . . . . . . . . . . . . . . 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 3579	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)
40	39	expr 456	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → (𝑥 = suc 𝑦 → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤))
41		iscard 9899	. . . . . . . . . . . . . . . . . . 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 5112	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ≺ 𝐴 ↔ 𝑤 ≺ (ℵ‘suc 𝑦)))
47	45, 46	sylibd 239	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → 𝑤 ≺ (ℵ‘suc 𝑦)))
48		alephnbtwn2 9994	. . . . . . . . . . . . . . . 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 3442   ⊆ wss 3903  ∅c0 4287   class class class wbr 5100  Oncon0 6325  Lim wlim 6326  suc csuc 6327  ‘cfv 6500  ωcom 7818   ≺ csdm 8894  cardccrd 9859  ℵcale 9860  cfccf 9861  Inacc_wcwina 10605

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 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-inf2 9562

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 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-int 4905  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-oi 9427  df-har 9474  df-card 9863  df-aleph 9864  df-cf 9865  df-wina 10607

This theorem is referenced by:  winafp  10620