Metamath Proof Explorer

Theorem limsucncmpi

Description: The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015)

Ref Expression
Hypothesis limsucncmpi.1 ⊢ Lim ⁡ A
Assertion limsucncmpi ⊢ ¬ suc ⁡ A ∈ Comp

Proof

Step Hyp Ref Expression
1 limsucncmpi.1 ⊢ Lim ⁡ A
2 elex ⊢ suc ⁡ A ∈ Top → suc ⁡ A ∈ V
3 sucexb ⊢ A ∈ V ↔ suc ⁡ A ∈ V
4 2 3 sylibr ⊢ suc ⁡ A ∈ Top → A ∈ V
5 sssucid ⊢ A ⊆ suc ⁡ A
6 elpwg ⊢ A ∈ V → A ∈ 𝒫 suc ⁡ A ↔ A ⊆ suc ⁡ A
7 5 6 mpbiri ⊢ A ∈ V → A ∈ 𝒫 suc ⁡ A
8 limuni ⊢ Lim ⁡ A → A = ⋃ A
9 1 8 ax-mp ⊢ A = ⋃ A
10 elin ⊢ z ∈ 𝒫 A ∩ Fin ↔ z ∈ 𝒫 A ∧ z ∈ Fin
11 elpwi ⊢ z ∈ 𝒫 A → z ⊆ A
12 11 anim1i ⊢ z ∈ 𝒫 A ∧ z ∈ Fin → z ⊆ A ∧ z ∈ Fin
13 10 12 sylbi ⊢ z ∈ 𝒫 A ∩ Fin → z ⊆ A ∧ z ∈ Fin
14 nlim0 ⊢ ¬ Lim ⁡ ∅
15 1 14 2th ⊢ Lim ⁡ A ↔ ¬ Lim ⁡ ∅
16 xor3 ⊢ ¬ Lim ⁡ A ↔ Lim ⁡ ∅ ↔ Lim ⁡ A ↔ ¬ Lim ⁡ ∅
17 15 16 mpbir ⊢ ¬ Lim ⁡ A ↔ Lim ⁡ ∅
18 limeq ⊢ A = ∅ → Lim ⁡ A ↔ Lim ⁡ ∅
19 18 necon3bi ⊢ ¬ Lim ⁡ A ↔ Lim ⁡ ∅ → A ≠ ∅
20 17 19 ax-mp ⊢ A ≠ ∅
21 uni0 ⊢ ⋃ ∅ = ∅
22 20 21 neeqtrri ⊢ A ≠ ⋃ ∅
23 unieq ⊢ z = ∅ → ⋃ z = ⋃ ∅
24 23 neeq2d ⊢ z = ∅ → A ≠ ⋃ z ↔ A ≠ ⋃ ∅
25 22 24 mpbiri ⊢ z = ∅ → A ≠ ⋃ z
26 25 a1i ⊢ z ⊆ A ∧ z ∈ Fin → z = ∅ → A ≠ ⋃ z
27 limord ⊢ Lim ⁡ A → Ord ⁡ A
28 ordsson ⊢ Ord ⁡ A → A ⊆ On
29 1 27 28 mp2b ⊢ A ⊆ On
30 sstr2 ⊢ z ⊆ A → A ⊆ On → z ⊆ On
31 29 30 mpi ⊢ z ⊆ A → z ⊆ On
32 ordunifi ⊢ z ⊆ On ∧ z ∈ Fin ∧ z ≠ ∅ → ⋃ z ∈ z
33 32 3expia ⊢ z ⊆ On ∧ z ∈ Fin → z ≠ ∅ → ⋃ z ∈ z
34 31 33 sylan ⊢ z ⊆ A ∧ z ∈ Fin → z ≠ ∅ → ⋃ z ∈ z
35 ssel ⊢ z ⊆ A → ⋃ z ∈ z → ⋃ z ∈ A
36 1 27 ax-mp ⊢ Ord ⁡ A
37 nordeq ⊢ Ord ⁡ A ∧ ⋃ z ∈ A → A ≠ ⋃ z
38 36 37 mpan ⊢ ⋃ z ∈ A → A ≠ ⋃ z
39 35 38 syl6 ⊢ z ⊆ A → ⋃ z ∈ z → A ≠ ⋃ z
40 39 adantr ⊢ z ⊆ A ∧ z ∈ Fin → ⋃ z ∈ z → A ≠ ⋃ z
41 34 40 syld ⊢ z ⊆ A ∧ z ∈ Fin → z ≠ ∅ → A ≠ ⋃ z
42 26 41 pm2.61dne ⊢ z ⊆ A ∧ z ∈ Fin → A ≠ ⋃ z
43 13 42 syl ⊢ z ∈ 𝒫 A ∩ Fin → A ≠ ⋃ z
44 43 neneqd ⊢ z ∈ 𝒫 A ∩ Fin → ¬ A = ⋃ z
45 44 nrex ⊢ ¬ ∃ z ∈ 𝒫 A ∩ Fin A = ⋃ z
46 unieq ⊢ y = A → ⋃ y = ⋃ A
47 46 eqeq2d ⊢ y = A → A = ⋃ y ↔ A = ⋃ A
48 pweq ⊢ y = A → 𝒫 y = 𝒫 A
49 48 ineq1d ⊢ y = A → 𝒫 y ∩ Fin = 𝒫 A ∩ Fin
50 49 rexeqdv ⊢ y = A → ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z ↔ ∃ z ∈ 𝒫 A ∩ Fin A = ⋃ z
51 50 notbid ⊢ y = A → ¬ ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z ↔ ¬ ∃ z ∈ 𝒫 A ∩ Fin A = ⋃ z
52 47 51 anbi12d ⊢ y = A → A = ⋃ y ∧ ¬ ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z ↔ A = ⋃ A ∧ ¬ ∃ z ∈ 𝒫 A ∩ Fin A = ⋃ z
53 52 rspcev ⊢ A ∈ 𝒫 suc ⁡ A ∧ A = ⋃ A ∧ ¬ ∃ z ∈ 𝒫 A ∩ Fin A = ⋃ z → ∃ y ∈ 𝒫 suc ⁡ A A = ⋃ y ∧ ¬ ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z
54 9 45 53 mpanr12 ⊢ A ∈ 𝒫 suc ⁡ A → ∃ y ∈ 𝒫 suc ⁡ A A = ⋃ y ∧ ¬ ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z
55 rexanali ⊢ ∃ y ∈ 𝒫 suc ⁡ A A = ⋃ y ∧ ¬ ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z ↔ ¬ ∀ y ∈ 𝒫 suc ⁡ A A = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z
56 54 55 sylib ⊢ A ∈ 𝒫 suc ⁡ A → ¬ ∀ y ∈ 𝒫 suc ⁡ A A = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z
57 4 7 56 3syl ⊢ suc ⁡ A ∈ Top → ¬ ∀ y ∈ 𝒫 suc ⁡ A A = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z
58 imnan ⊢ suc ⁡ A ∈ Top → ¬ ∀ y ∈ 𝒫 suc ⁡ A A = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z ↔ ¬ suc ⁡ A ∈ Top ∧ ∀ y ∈ 𝒫 suc ⁡ A A = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z
59 57 58 mpbi ⊢ ¬ suc ⁡ A ∈ Top ∧ ∀ y ∈ 𝒫 suc ⁡ A A = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z
60 ordunisuc ⊢ Ord ⁡ A → ⋃ suc ⁡ A = A
61 1 27 60 mp2b ⊢ ⋃ suc ⁡ A = A
62 61 eqcomi ⊢ A = ⋃ suc ⁡ A
63 62 iscmp ⊢ suc ⁡ A ∈ Comp ↔ suc ⁡ A ∈ Top ∧ ∀ y ∈ 𝒫 suc ⁡ A A = ⋃ y → ∃ z ∈ 𝒫 y ∩ Fin A = ⋃ z
64 59 63 mtbir ⊢ ¬ suc ⁡ A ∈ Comp