This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 onsuc ⊢ ( 𝑧 ∈ 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 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≺ 𝑦 ) → ω ⊆ 𝐴 )