Metamath Proof Explorer

Theorem lly1stc

Description: First-countability is a local property (unlike second-countability). (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion lly1stc 
|- Locally 1stc = 1stc

Proof

Step Hyp Ref Expression
1 llytop 
 |-  ( j e. Locally 1stc -> j e. Top )
2 simprr 
 |-  ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) -> ( j |`t u ) e. 1stc )
3 simprl 
 |-  ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) -> x e. u )
4 1 ad3antrrr 
 |-  ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) -> j e. Top )
5 elssuni 
 |-  ( u e. j -> u C_ U. j )
6 5 ad2antlr 
 |-  ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) -> u C_ U. j )
7 eqid 
 |-  U. j = U. j
8 7 restuni 
 |-  ( ( j e. Top /\ u C_ U. j ) -> u = U. ( j |`t u ) )
9 4 6 8 syl2anc 
 |-  ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) -> u = U. ( j |`t u ) )
10 3 9 eleqtrd 
 |-  ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) -> x e. U. ( j |`t u ) )
11 eqid 
 |-  U. ( j |`t u ) = U. ( j |`t u )
12 11 1stcclb 
 |-  ( ( ( j |`t u ) e. 1stc /\ x e. U. ( j |`t u ) ) -> E. t e. ~P ( j |`t u ) ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) )
13 2 10 12 syl2anc 
 |-  ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) -> E. t e. ~P ( j |`t u ) ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) )
14 elpwi 
 |-  ( t e. ~P ( j |`t u ) -> t C_ ( j |`t u ) )
15 14 adantl 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) -> t C_ ( j |`t u ) )
16 15 sselda 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> n e. ( j |`t u ) )
17 4 adantr 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) -> j e. Top )
18 simpllr 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) -> u e. j )
19 restopn2 
 |-  ( ( j e. Top /\ u e. j ) -> ( n e. ( j |`t u ) <-> ( n e. j /\ n C_ u ) ) )
20 17 18 19 syl2anc 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) -> ( n e. ( j |`t u ) <-> ( n e. j /\ n C_ u ) ) )
21 20 simplbda 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. ( j |`t u ) ) -> n C_ u )
22 16 21 syldan 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> n C_ u )
23 df-ss 
 |-  ( n C_ u <-> ( n i^i u ) = n )
24 22 23 sylib 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> ( n i^i u ) = n )
25 20 simprbda 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. ( j |`t u ) ) -> n e. j )
26 16 25 syldan 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> n e. j )
27 24 26 eqeltrd 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> ( n i^i u ) e. j )
28 ineq1 
 |-  ( a = n -> ( a i^i u ) = ( n i^i u ) )
29 28 cbvmptv 
 |-  ( a e. t |-> ( a i^i u ) ) = ( n e. t |-> ( n i^i u ) )
30 27 29 fmptd 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) -> ( a e. t |-> ( a i^i u ) ) : t --> j )
31 30 frnd 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) -> ran ( a e. t |-> ( a i^i u ) ) C_ j )
32 31 adantrr 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) -> ran ( a e. t |-> ( a i^i u ) ) C_ j )
33 vex 
 |-  j e. _V
34 33 elpw2 
 |-  ( ran ( a e. t |-> ( a i^i u ) ) e. ~P j <-> ran ( a e. t |-> ( a i^i u ) ) C_ j )
35 32 34 sylibr 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) -> ran ( a e. t |-> ( a i^i u ) ) e. ~P j )
36 simprrl 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) -> t ~<_ _om )
37 1stcrestlem 
 |-  ( t ~<_ _om -> ran ( a e. t |-> ( a i^i u ) ) ~<_ _om )
38 36 37 syl 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) -> ran ( a e. t |-> ( a i^i u ) ) ~<_ _om )
39 simprr 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> x e. z )
40 3 ad2antrr 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> x e. u )
41 39 40 elind 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> x e. ( z i^i u ) )
42 eleq2 
 |-  ( v = ( z i^i u ) -> ( x e. v <-> x e. ( z i^i u ) ) )
43 sseq2 
 |-  ( v = ( z i^i u ) -> ( n C_ v <-> n C_ ( z i^i u ) ) )
44 43 anbi2d 
 |-  ( v = ( z i^i u ) -> ( ( x e. n /\ n C_ v ) <-> ( x e. n /\ n C_ ( z i^i u ) ) ) )
45 44 rexbidv 
 |-  ( v = ( z i^i u ) -> ( E. n e. t ( x e. n /\ n C_ v ) <-> E. n e. t ( x e. n /\ n C_ ( z i^i u ) ) ) )
46 42 45 imbi12d 
 |-  ( v = ( z i^i u ) -> ( ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) <-> ( x e. ( z i^i u ) -> E. n e. t ( x e. n /\ n C_ ( z i^i u ) ) ) ) )
47 simprrr 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) -> A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) )
48 47 adantr 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) )
49 4 ad2antrr 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> j e. Top )
50 simpllr 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) -> u e. j )
51 50 adantr 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> u e. j )
52 simprl 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> z e. j )
53 elrestr 
 |-  ( ( j e. Top /\ u e. j /\ z e. j ) -> ( z i^i u ) e. ( j |`t u ) )
54 49 51 52 53 syl3anc 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> ( z i^i u ) e. ( j |`t u ) )
55 46 48 54 rspcdva 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> ( x e. ( z i^i u ) -> E. n e. t ( x e. n /\ n C_ ( z i^i u ) ) ) )
56 41 55 mpd 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> E. n e. t ( x e. n /\ n C_ ( z i^i u ) ) )
57 3 ad2antrr 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> x e. u )
58 elin 
 |-  ( x e. ( n i^i u ) <-> ( x e. n /\ x e. u ) )
59 58 simplbi2com 
 |-  ( x e. u -> ( x e. n -> x e. ( n i^i u ) ) )
60 57 59 syl 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> ( x e. n -> x e. ( n i^i u ) ) )
61 22 biantrud 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> ( n C_ z <-> ( n C_ z /\ n C_ u ) ) )
62 ssin 
 |-  ( ( n C_ z /\ n C_ u ) <-> n C_ ( z i^i u ) )
63 61 62 bitrdi 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> ( n C_ z <-> n C_ ( z i^i u ) ) )
64 ssinss1 
 |-  ( n C_ z -> ( n i^i u ) C_ z )
65 63 64 syl6bir 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> ( n C_ ( z i^i u ) -> ( n i^i u ) C_ z ) )
66 60 65 anim12d 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) /\ n e. t ) -> ( ( x e. n /\ n C_ ( z i^i u ) ) -> ( x e. ( n i^i u ) /\ ( n i^i u ) C_ z ) ) )
67 66 reximdva 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) -> ( E. n e. t ( x e. n /\ n C_ ( z i^i u ) ) -> E. n e. t ( x e. ( n i^i u ) /\ ( n i^i u ) C_ z ) ) )
68 vex 
 |-  n e. _V
69 68 inex1 
 |-  ( n i^i u ) e. _V
70 69 rgenw 
 |-  A. n e. t ( n i^i u ) e. _V
71 eleq2 
 |-  ( w = ( n i^i u ) -> ( x e. w <-> x e. ( n i^i u ) ) )
72 sseq1 
 |-  ( w = ( n i^i u ) -> ( w C_ z <-> ( n i^i u ) C_ z ) )
73 71 72 anbi12d 
 |-  ( w = ( n i^i u ) -> ( ( x e. w /\ w C_ z ) <-> ( x e. ( n i^i u ) /\ ( n i^i u ) C_ z ) ) )
74 29 73 rexrnmptw 
 |-  ( A. n e. t ( n i^i u ) e. _V -> ( E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) <-> E. n e. t ( x e. ( n i^i u ) /\ ( n i^i u ) C_ z ) ) )
75 70 74 ax-mp 
 |-  ( E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) <-> E. n e. t ( x e. ( n i^i u ) /\ ( n i^i u ) C_ z ) )
76 67 75 syl6ibr 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ t e. ~P ( j |`t u ) ) -> ( E. n e. t ( x e. n /\ n C_ ( z i^i u ) ) -> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) ) )
77 76 adantrr 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) -> ( E. n e. t ( x e. n /\ n C_ ( z i^i u ) ) -> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) ) )
78 77 adantr 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> ( E. n e. t ( x e. n /\ n C_ ( z i^i u ) ) -> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) ) )
79 56 78 mpd 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ ( z e. j /\ x e. z ) ) -> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) )
80 79 expr 
 |-  ( ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) /\ z e. j ) -> ( x e. z -> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) ) )
81 80 ralrimiva 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) -> A. z e. j ( x e. z -> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) ) )
82 breq1 
 |-  ( y = ran ( a e. t |-> ( a i^i u ) ) -> ( y ~<_ _om <-> ran ( a e. t |-> ( a i^i u ) ) ~<_ _om ) )
83 rexeq 
 |-  ( y = ran ( a e. t |-> ( a i^i u ) ) -> ( E. w e. y ( x e. w /\ w C_ z ) <-> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) ) )
84 83 imbi2d 
 |-  ( y = ran ( a e. t |-> ( a i^i u ) ) -> ( ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) <-> ( x e. z -> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) ) ) )
85 84 ralbidv 
 |-  ( y = ran ( a e. t |-> ( a i^i u ) ) -> ( A. z e. j ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) <-> A. z e. j ( x e. z -> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) ) ) )
86 82 85 anbi12d 
 |-  ( y = ran ( a e. t |-> ( a i^i u ) ) -> ( ( y ~<_ _om /\ A. z e. j ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) <-> ( ran ( a e. t |-> ( a i^i u ) ) ~<_ _om /\ A. z e. j ( x e. z -> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) ) ) ) )
87 86 rspcev 
 |-  ( ( ran ( a e. t |-> ( a i^i u ) ) e. ~P j /\ ( ran ( a e. t |-> ( a i^i u ) ) ~<_ _om /\ A. z e. j ( x e. z -> E. w e. ran ( a e. t |-> ( a i^i u ) ) ( x e. w /\ w C_ z ) ) ) ) -> E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
88 35 38 81 87 syl12anc 
 |-  ( ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) /\ ( t e. ~P ( j |`t u ) /\ ( t ~<_ _om /\ A. v e. ( j |`t u ) ( x e. v -> E. n e. t ( x e. n /\ n C_ v ) ) ) ) ) -> E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
89 13 88 rexlimddv 
 |-  ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( x e. u /\ ( j |`t u ) e. 1stc ) ) -> E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
90 89 3adantr1 
 |-  ( ( ( ( j e. Locally 1stc /\ x e. U. j ) /\ u e. j ) /\ ( u C_ U. j /\ x e. u /\ ( j |`t u ) e. 1stc ) ) -> E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
91 simpl 
 |-  ( ( j e. Locally 1stc /\ x e. U. j ) -> j e. Locally 1stc )
92 1 adantr 
 |-  ( ( j e. Locally 1stc /\ x e. U. j ) -> j e. Top )
93 7 topopn 
 |-  ( j e. Top -> U. j e. j )
94 92 93 syl 
 |-  ( ( j e. Locally 1stc /\ x e. U. j ) -> U. j e. j )
95 simpr 
 |-  ( ( j e. Locally 1stc /\ x e. U. j ) -> x e. U. j )
96 llyi 
 |-  ( ( j e. Locally 1stc /\ U. j e. j /\ x e. U. j ) -> E. u e. j ( u C_ U. j /\ x e. u /\ ( j |`t u ) e. 1stc ) )
97 91 94 95 96 syl3anc 
 |-  ( ( j e. Locally 1stc /\ x e. U. j ) -> E. u e. j ( u C_ U. j /\ x e. u /\ ( j |`t u ) e. 1stc ) )
98 90 97 r19.29a 
 |-  ( ( j e. Locally 1stc /\ x e. U. j ) -> E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
99 98 ralrimiva 
 |-  ( j e. Locally 1stc -> A. x e. U. j E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
100 7 is1stc2 
 |-  ( j e. 1stc <-> ( j e. Top /\ A. x e. U. j E. y e. ~P j ( y ~<_ _om /\ A. z e. j ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) ) )
101 1 99 100 sylanbrc 
 |-  ( j e. Locally 1stc -> j e. 1stc )
102 101 ssriv 
 |-  Locally 1stc C_ 1stc
103 1stcrest 
 |-  ( ( j e. 1stc /\ x e. j ) -> ( j |`t x ) e. 1stc )
104 103 adantl 
 |-  ( ( T. /\ ( j e. 1stc /\ x e. j ) ) -> ( j |`t x ) e. 1stc )
105 1stctop 
 |-  ( j e. 1stc -> j e. Top )
106 105 ssriv 
 |-  1stc C_ Top
107 106 a1i 
 |-  ( T. -> 1stc C_ Top )
108 104 107 restlly 
 |-  ( T. -> 1stc C_ Locally 1stc )
109 108 mptru 
 |-  1stc C_ Locally 1stc
110 102 109 eqssi 
 |-  Locally 1stc = 1stc