Theorem winalim2 10687

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 10683	. . . 4 ⊢ (𝐴 ∈ Inaccw → (card‘𝐴) = 𝐴)
2		winainf 10685	. . . . 5 ⊢ (𝐴 ∈ Inaccw → ω ⊆ 𝐴)
3		cardalephex 10081	. . . . 5 ⊢ (ω ⊆ 𝐴 → ((card‘𝐴) = 𝐴 ↔ ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥)))
4	2, 3	syl 17	. . . 4 ⊢ (𝐴 ∈ Inaccw → ((card‘𝐴) = 𝐴 ↔ ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥)))
5	1, 4	mpbid 231	. . 3 ⊢ (𝐴 ∈ Inaccw → ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥))
6	5	adantr 481	. 2 ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥))
7		df-rex 3071	. . 3 ⊢ (∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥) ↔ ∃𝑥(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥)))
8		simprr 771	. . . . . . 7 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝐴 = (ℵ‘𝑥))
9	8	eqcomd 2738	. . . . . 6 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (ℵ‘𝑥) = 𝐴)
10		simprl 769	. . . . . . . 8 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝑥 ∈ On)
11		onzsl 7831	. . . . . . . 8 ⊢ (𝑥 ∈ On ↔ (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥)))
12	10, 11	sylib 217	. . . . . . 7 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥)))
13		simplr 767	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → 𝐴 ≠ ω)
14		fveq2 6888	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (ℵ‘𝑥) = (ℵ‘∅))
15		aleph0 10057	. . . . . . . . . . . . . 14 ⊢ (ℵ‘∅) = ω
16	14, 15	eqtrdi 2788	. . . . . . . . . . . . 13 ⊢ (𝑥 = ∅ → (ℵ‘𝑥) = ω)
17		eqtr 2755	. . . . . . . . . . . . 13 ⊢ ((𝐴 = (ℵ‘𝑥) ∧ (ℵ‘𝑥) = ω) → 𝐴 = ω)
18	16, 17	sylan2 593	. . . . . . . . . . . 12 ⊢ ((𝐴 = (ℵ‘𝑥) ∧ 𝑥 = ∅) → 𝐴 = ω)
19	18	ex 413	. . . . . . . . . . 11 ⊢ (𝐴 = (ℵ‘𝑥) → (𝑥 = ∅ → 𝐴 = ω))
20	19	necon3ad 2953	. . . . . . . . . 10 ⊢ (𝐴 = (ℵ‘𝑥) → (𝐴 ≠ ω → ¬ 𝑥 = ∅))
21	8, 13, 20	sylc 65	. . . . . . . . 9 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ¬ 𝑥 = ∅)
22	21	pm2.21d 121	. . . . . . . 8 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (𝑥 = ∅ → Lim 𝑥))
23		breq1 5150	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (ℵ‘𝑦) → (𝑧 ≺ 𝑤 ↔ (ℵ‘𝑦) ≺ 𝑤))
24	23	rexbidv 3178	. . . . . . . . . . . . 13 ⊢ (𝑧 = (ℵ‘𝑦) → (∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 ↔ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤))
25		elwina 10677	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ Inaccw ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤))
26	25	simp3bi 1147	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ Inaccw → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)
27	26	ad3antrrr 728	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐴 𝑧 ≺ 𝑤)
28		onsuc 7795	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ On → suc 𝑦 ∈ On)
29		vex 3478	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
30	29	sucid 6443	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ suc 𝑦
31		alephord2i 10068	. . . . . . . . . . . . . . . 16 ⊢ (suc 𝑦 ∈ On → (𝑦 ∈ suc 𝑦 → (ℵ‘𝑦) ∈ (ℵ‘suc 𝑦)))
32	28, 30, 31	mpisyl 21	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ On → (ℵ‘𝑦) ∈ (ℵ‘suc 𝑦))
33	32	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑦) ∈ (ℵ‘suc 𝑦))
34		simplrr 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → 𝐴 = (ℵ‘𝑥))
35		fveq2 6888	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑦 → (ℵ‘𝑥) = (ℵ‘suc 𝑦))
36	35	ad2antll 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑥) = (ℵ‘suc 𝑦))
37	34, 36	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → 𝐴 = (ℵ‘suc 𝑦))
38	33, 37	eleqtrrd 2836	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (ℵ‘𝑦) ∈ 𝐴)
39	24, 27, 38	rspcdva 3613	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)
40	39	expr 457	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → (𝑥 = suc 𝑦 → ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤))
41		iscard 9966	. . . . . . . . . . . . . . . . . . 19 ⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑤 ∈ 𝐴 𝑤 ≺ 𝐴))
42	41	simprbi 497	. . . . . . . . . . . . . . . . . 18 ⊢ ((card‘𝐴) = 𝐴 → ∀𝑤 ∈ 𝐴 𝑤 ≺ 𝐴)
43		rsp 3244	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ 𝐴 𝑤 ≺ 𝐴 → (𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴))
44	1, 42, 43	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ Inaccw → (𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴))
45	44	ad3antrrr 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → 𝑤 ≺ 𝐴))
46	37	breq2d 5159	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ≺ 𝐴 ↔ 𝑤 ≺ (ℵ‘suc 𝑦)))
47	45, 46	sylibd 238	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → 𝑤 ≺ (ℵ‘suc 𝑦)))
48		alephnbtwn2 10063	. . . . . . . . . . . . . . . 16 ⊢ ¬ ((ℵ‘𝑦) ≺ 𝑤 ∧ 𝑤 ≺ (ℵ‘suc 𝑦))
49		pm3.21 472	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ≺ (ℵ‘suc 𝑦) → ((ℵ‘𝑦) ≺ 𝑤 → ((ℵ‘𝑦) ≺ 𝑤 ∧ 𝑤 ≺ (ℵ‘suc 𝑦))))
50	48, 49	mtoi 198	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ≺ (ℵ‘suc 𝑦) → ¬ (ℵ‘𝑦) ≺ 𝑤)
51	47, 50	syl6 35	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → (𝑤 ∈ 𝐴 → ¬ (ℵ‘𝑦) ≺ 𝑤))
52	51	imp 407	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) ∧ 𝑤 ∈ 𝐴) → ¬ (ℵ‘𝑦) ≺ 𝑤)
53	52	nrexdv 3149	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ (𝑦 ∈ On ∧ 𝑥 = suc 𝑦)) → ¬ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤)
54	53	expr 457	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → (𝑥 = suc 𝑦 → ¬ ∃𝑤 ∈ 𝐴 (ℵ‘𝑦) ≺ 𝑤))
55	40, 54	pm2.65d 195	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) ∧ 𝑦 ∈ On) → ¬ 𝑥 = suc 𝑦)
56	55	nrexdv 3149	. . . . . . . . 9 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ¬ ∃𝑦 ∈ On 𝑥 = suc 𝑦)
57	56	pm2.21d 121	. . . . . . . 8 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → (∃𝑦 ∈ On 𝑥 = suc 𝑦 → Lim 𝑥))
58		simpr 485	. . . . . . . . 9 ⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → Lim 𝑥)
59	58	a1i 11	. . . . . . . 8 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((𝑥 ∈ V ∧ Lim 𝑥) → Lim 𝑥))
60	22, 57, 59	3jaod 1428	. . . . . . 7 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((𝑥 = ∅ ∨ ∃𝑦 ∈ On 𝑥 = suc 𝑦 ∨ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim 𝑥))
61	12, 60	mpd 15	. . . . . 6 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → Lim 𝑥)
62	9, 61	jca 512	. . . . 5 ⊢ (((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) ∧ (𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥))) → ((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))
63	62	ex 413	. . . 4 ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ((𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥)) → ((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)))
64	63	eximdv 1920	. . 3 ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → (∃𝑥(𝑥 ∈ On ∧ 𝐴 = (ℵ‘𝑥)) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)))
65	7, 64	biimtrid 241	. 2 ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → (∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥)))
66	6, 65	mpd 15	1 ⊢ ((𝐴 ∈ Inaccw ∧ 𝐴 ≠ ω) → ∃𝑥((ℵ‘𝑥) = 𝐴 ∧ Lim 𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1086   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  Vcvv 3474   ⊆ wss 3947  ∅c0 4321   class class class wbr 5147  Oncon0 6361  Lim wlim 6362  suc csuc 6363  ‘cfv 6540  ωcom 7851   ≺ csdm 8934  cardccrd 9926  ℵcale 9927  cfccf 9928  Inacc_wcwina 10673

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-oi 9501  df-har 9548  df-card 9930  df-aleph 9931  df-cf 9932  df-wina 10675

This theorem is referenced by:  winafp  10688