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 𝐴
Assertion limsucncmpi ¬ suc 𝐴 ∈ Comp

Proof

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