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 e. Comp

Proof

Step Hyp Ref Expression
1 limsucncmpi.1 
 |-  Lim A
2 elex 
 |-  ( suc A e. Top -> suc A e. _V )
3 sucexb 
 |-  ( A e. _V <-> suc A e. _V )
4 2 3 sylibr 
 |-  ( suc A e. Top -> A e. _V )
5 sssucid 
 |-  A C_ suc A
6 elpwg 
 |-  ( A e. _V -> ( A e. ~P suc A <-> A C_ suc A ) )
7 5 6 mpbiri 
 |-  ( A e. _V -> A e. ~P suc A )
8 limuni 
 |-  ( Lim A -> A = U. A )
9 1 8 ax-mp 
 |-  A = U. A
10 elin 
 |-  ( z e. ( ~P A i^i Fin ) <-> ( z e. ~P A /\ z e. Fin ) )
11 elpwi 
 |-  ( z e. ~P A -> z C_ A )
12 11 anim1i 
 |-  ( ( z e. ~P A /\ z e. Fin ) -> ( z C_ A /\ z e. Fin ) )
13 10 12 sylbi 
 |-  ( z e. ( ~P A i^i Fin ) -> ( z C_ A /\ z e. 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 
 |-  U. (/) = (/)
22 20 21 neeqtrri 
 |-  A =/= U. (/)
23 unieq 
 |-  ( z = (/) -> U. z = U. (/) )
24 23 neeq2d 
 |-  ( z = (/) -> ( A =/= U. z <-> A =/= U. (/) ) )
25 22 24 mpbiri 
 |-  ( z = (/) -> A =/= U. z )
26 25 a1i 
 |-  ( ( z C_ A /\ z e. Fin ) -> ( z = (/) -> A =/= U. z ) )
27 limord 
 |-  ( Lim A -> Ord A )
28 ordsson 
 |-  ( Ord A -> A C_ On )
29 1 27 28 mp2b 
 |-  A C_ On
30 sstr2 
 |-  ( z C_ A -> ( A C_ On -> z C_ On ) )
31 29 30 mpi 
 |-  ( z C_ A -> z C_ On )
32 ordunifi 
 |-  ( ( z C_ On /\ z e. Fin /\ z =/= (/) ) -> U. z e. z )
33 32 3expia 
 |-  ( ( z C_ On /\ z e. Fin ) -> ( z =/= (/) -> U. z e. z ) )
34 31 33 sylan 
 |-  ( ( z C_ A /\ z e. Fin ) -> ( z =/= (/) -> U. z e. z ) )
35 ssel 
 |-  ( z C_ A -> ( U. z e. z -> U. z e. A ) )
36 1 27 ax-mp 
 |-  Ord A
37 nordeq 
 |-  ( ( Ord A /\ U. z e. A ) -> A =/= U. z )
38 36 37 mpan 
 |-  ( U. z e. A -> A =/= U. z )
39 35 38 syl6 
 |-  ( z C_ A -> ( U. z e. z -> A =/= U. z ) )
40 39 adantr 
 |-  ( ( z C_ A /\ z e. Fin ) -> ( U. z e. z -> A =/= U. z ) )
41 34 40 syld 
 |-  ( ( z C_ A /\ z e. Fin ) -> ( z =/= (/) -> A =/= U. z ) )
42 26 41 pm2.61dne 
 |-  ( ( z C_ A /\ z e. Fin ) -> A =/= U. z )
43 13 42 syl 
 |-  ( z e. ( ~P A i^i Fin ) -> A =/= U. z )
44 43 neneqd 
 |-  ( z e. ( ~P A i^i Fin ) -> -. A = U. z )
45 44 nrex 
 |-  -. E. z e. ( ~P A i^i Fin ) A = U. z
46 unieq 
 |-  ( y = A -> U. y = U. A )
47 46 eqeq2d 
 |-  ( y = A -> ( A = U. y <-> A = U. A ) )
48 pweq 
 |-  ( y = A -> ~P y = ~P A )
49 48 ineq1d 
 |-  ( y = A -> ( ~P y i^i Fin ) = ( ~P A i^i Fin ) )
50 49 rexeqdv 
 |-  ( y = A -> ( E. z e. ( ~P y i^i Fin ) A = U. z <-> E. z e. ( ~P A i^i Fin ) A = U. z ) )
51 50 notbid 
 |-  ( y = A -> ( -. E. z e. ( ~P y i^i Fin ) A = U. z <-> -. E. z e. ( ~P A i^i Fin ) A = U. z ) )
52 47 51 anbi12d 
 |-  ( y = A -> ( ( A = U. y /\ -. E. z e. ( ~P y i^i Fin ) A = U. z ) <-> ( A = U. A /\ -. E. z e. ( ~P A i^i Fin ) A = U. z ) ) )
53 52 rspcev 
 |-  ( ( A e. ~P suc A /\ ( A = U. A /\ -. E. z e. ( ~P A i^i Fin ) A = U. z ) ) -> E. y e. ~P suc A ( A = U. y /\ -. E. z e. ( ~P y i^i Fin ) A = U. z ) )
54 9 45 53 mpanr12 
 |-  ( A e. ~P suc A -> E. y e. ~P suc A ( A = U. y /\ -. E. z e. ( ~P y i^i Fin ) A = U. z ) )
55 rexanali 
 |-  ( E. y e. ~P suc A ( A = U. y /\ -. E. z e. ( ~P y i^i Fin ) A = U. z ) <-> -. A. y e. ~P suc A ( A = U. y -> E. z e. ( ~P y i^i Fin ) A = U. z ) )
56 54 55 sylib 
 |-  ( A e. ~P suc A -> -. A. y e. ~P suc A ( A = U. y -> E. z e. ( ~P y i^i Fin ) A = U. z ) )
57 4 7 56 3syl 
 |-  ( suc A e. Top -> -. A. y e. ~P suc A ( A = U. y -> E. z e. ( ~P y i^i Fin ) A = U. z ) )
58 imnan 
 |-  ( ( suc A e. Top -> -. A. y e. ~P suc A ( A = U. y -> E. z e. ( ~P y i^i Fin ) A = U. z ) ) <-> -. ( suc A e. Top /\ A. y e. ~P suc A ( A = U. y -> E. z e. ( ~P y i^i Fin ) A = U. z ) ) )
59 57 58 mpbi 
 |-  -. ( suc A e. Top /\ A. y e. ~P suc A ( A = U. y -> E. z e. ( ~P y i^i Fin ) A = U. z ) )
60 ordunisuc 
 |-  ( Ord A -> U. suc A = A )
61 1 27 60 mp2b 
 |-  U. suc A = A
62 61 eqcomi 
 |-  A = U. suc A
63 62 iscmp 
 |-  ( suc A e. Comp <-> ( suc A e. Top /\ A. y e. ~P suc A ( A = U. y -> E. z e. ( ~P y i^i Fin ) A = U. z ) ) )
64 59 63 mtbir 
 |-  -. suc A e. Comp