Theorem winainflem

Description: A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014)

	Ref	Expression
Assertion	winainflem	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → ω ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nn0suc	⊢ ( 𝐴 ∈ ω → ( 𝐴 = ∅ ∨ ∃ 𝑧 ∈ ω 𝐴 = suc 𝑧 ) )
2		simp1	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → 𝐴 ≠ ∅ )
3	2	necon2bi	⊢ ( 𝐴 = ∅ → ¬ ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
4		vex	⊢ 𝑧 ∈ V
5	4	sucid	⊢ 𝑧 ∈ suc 𝑧
6		eleq2	⊢ ( 𝐴 = suc 𝑧 → ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ suc 𝑧 ) )
7	5 6	mpbiri	⊢ ( 𝐴 = suc 𝑧 → 𝑧 ∈ 𝐴 )
8	7	adantl	⊢ ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ) → 𝑧 ∈ 𝐴 )
9		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≺ 𝑦 ↔ 𝑧 ≺ 𝑦 ) )
10	9	rexbidv	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑧 ≺ 𝑦 ) )
11		breq2	⊢ ( 𝑦 = 𝑤 → ( 𝑧 ≺ 𝑦 ↔ 𝑧 ≺ 𝑤 ) )
12	11	cbvrexvw	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑧 ≺ 𝑦 ↔ ∃ 𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 )
13	10 12	bitrdi	⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ↔ ∃ 𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 ) )
14	13	rspcv	⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 → ∃ 𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 ) )
15	8 14	syl	⊢ ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 → ∃ 𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 ) )
16		eleq2	⊢ ( 𝐴 = suc 𝑧 → ( 𝑤 ∈ 𝐴 ↔ 𝑤 ∈ suc 𝑧 ) )
17	16	biimpa	⊢ ( ( 𝐴 = suc 𝑧 ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ suc 𝑧 )
18	17	3ad2antl2	⊢ ( ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ suc 𝑧 )
19		nnon	⊢ ( 𝑧 ∈ ω → 𝑧 ∈ On )
20		suceloni	⊢ ( 𝑧 ∈ On → suc 𝑧 ∈ On )
21	19 20	syl	⊢ ( 𝑧 ∈ ω → suc 𝑧 ∈ On )
22		eleq1	⊢ ( 𝐴 = suc 𝑧 → ( 𝐴 ∈ On ↔ suc 𝑧 ∈ On ) )
23	22	biimparc	⊢ ( ( suc 𝑧 ∈ On ∧ 𝐴 = suc 𝑧 ) → 𝐴 ∈ On )
24	21 23	sylan	⊢ ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ) → 𝐴 ∈ On )
25	24	3adant3	⊢ ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → 𝐴 ∈ On )
26		onelon	⊢ ( ( 𝐴 ∈ On ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ On )
27	25 26	sylan	⊢ ( ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ On )
28		simpl1	⊢ ( ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ∧ 𝑤 ∈ 𝐴 ) → 𝑧 ∈ ω )
29	28 19	syl	⊢ ( ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ∧ 𝑤 ∈ 𝐴 ) → 𝑧 ∈ On )
30		onsssuc	⊢ ( ( 𝑤 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑤 ⊆ 𝑧 ↔ 𝑤 ∈ suc 𝑧 ) )
31	27 29 30	syl2anc	⊢ ( ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 ⊆ 𝑧 ↔ 𝑤 ∈ suc 𝑧 ) )
32	18 31	mpbird	⊢ ( ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ⊆ 𝑧 )
33		ssdomg	⊢ ( 𝑧 ∈ V → ( 𝑤 ⊆ 𝑧 → 𝑤 ≼ 𝑧 ) )
34	4 32 33	mpsyl	⊢ ( ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ≼ 𝑧 )
35		domnsym	⊢ ( 𝑤 ≼ 𝑧 → ¬ 𝑧 ≺ 𝑤 )
36	34 35	syl	⊢ ( ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) ∧ 𝑤 ∈ 𝐴 ) → ¬ 𝑧 ≺ 𝑤 )
37	36	nrexdv	⊢ ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → ¬ ∃ 𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 )
38	37	3expia	⊢ ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 → ¬ ∃ 𝑤 ∈ 𝐴 𝑧 ≺ 𝑤 ) )
39	15 38	pm2.65d	⊢ ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ) → ¬ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 )
40	39	intn3an3d	⊢ ( ( 𝑧 ∈ ω ∧ 𝐴 = suc 𝑧 ) → ¬ ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
41	40	rexlimiva	⊢ ( ∃ 𝑧 ∈ ω 𝐴 = suc 𝑧 → ¬ ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
42	3 41	jaoi	⊢ ( ( 𝐴 = ∅ ∨ ∃ 𝑧 ∈ ω 𝐴 = suc 𝑧 ) → ¬ ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
43	1 42	syl	⊢ ( 𝐴 ∈ ω → ¬ ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) )
44	43	con2i	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → ¬ 𝐴 ∈ ω )
45		ordom	⊢ Ord ω
46		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
47	46	3ad2ant2	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → Ord 𝐴 )
48		ordtri1	⊢ ( ( Ord ω ∧ Ord 𝐴 ) → ( ω ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ω ) )
49	45 47 48	sylancr	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → ( ω ⊆ 𝐴 ↔ ¬ 𝐴 ∈ ω ) )
50	44 49	mpbird	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐴 ∈ On ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → ω ⊆ 𝐴 )