Metamath Proof Explorer

Theorem 1stcrest

Description: A subspace of a first-countable space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Assertion 1stcrest 
|- ( ( J e. 1stc /\ A e. V ) -> ( J |`t A ) e. 1stc )

Proof

Step Hyp Ref Expression
1 1stctop 
 |-  ( J e. 1stc -> J e. Top )
2 resttop 
 |-  ( ( J e. Top /\ A e. V ) -> ( J |`t A ) e. Top )
3 1 2 sylan 
 |-  ( ( J e. 1stc /\ A e. V ) -> ( J |`t A ) e. Top )
4 eqid 
 |-  U. J = U. J
5 4 restuni2 
 |-  ( ( J e. Top /\ A e. V ) -> ( A i^i U. J ) = U. ( J |`t A ) )
6 1 5 sylan 
 |-  ( ( J e. 1stc /\ A e. V ) -> ( A i^i U. J ) = U. ( J |`t A ) )
7 6 eleq2d 
 |-  ( ( J e. 1stc /\ A e. V ) -> ( x e. ( A i^i U. J ) <-> x e. U. ( J |`t A ) ) )
8 7 biimpar 
 |-  ( ( ( J e. 1stc /\ A e. V ) /\ x e. U. ( J |`t A ) ) -> x e. ( A i^i U. J ) )
9 simpl 
 |-  ( ( J e. 1stc /\ A e. V ) -> J e. 1stc )
10 elinel2 
 |-  ( x e. ( A i^i U. J ) -> x e. U. J )
11 4 1stcclb 
 |-  ( ( J e. 1stc /\ x e. U. J ) -> E. t e. ~P J ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) )
12 9 10 11 syl2an 
 |-  ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) -> E. t e. ~P J ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) )
13 simplll 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> J e. 1stc )
14 elpwi 
 |-  ( t e. ~P J -> t C_ J )
15 14 ad2antrl 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> t C_ J )
16 ssrest 
 |-  ( ( J e. 1stc /\ t C_ J ) -> ( t |`t A ) C_ ( J |`t A ) )
17 13 15 16 syl2anc 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> ( t |`t A ) C_ ( J |`t A ) )
18 ovex 
 |-  ( J |`t A ) e. _V
19 18 elpw2 
 |-  ( ( t |`t A ) e. ~P ( J |`t A ) <-> ( t |`t A ) C_ ( J |`t A ) )
20 17 19 sylibr 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> ( t |`t A ) e. ~P ( J |`t A ) )
21 vex 
 |-  t e. _V
22 simpllr 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> A e. V )
23 restval 
 |-  ( ( t e. _V /\ A e. V ) -> ( t |`t A ) = ran ( v e. t |-> ( v i^i A ) ) )
24 21 22 23 sylancr 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> ( t |`t A ) = ran ( v e. t |-> ( v i^i A ) ) )
25 simprrl 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> t ~<_ _om )
26 1stcrestlem 
 |-  ( t ~<_ _om -> ran ( v e. t |-> ( v i^i A ) ) ~<_ _om )
27 25 26 syl 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> ran ( v e. t |-> ( v i^i A ) ) ~<_ _om )
28 24 27 eqbrtrd 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> ( t |`t A ) ~<_ _om )
29 1 ad3antrrr 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> J e. Top )
30 elrest 
 |-  ( ( J e. Top /\ A e. V ) -> ( z e. ( J |`t A ) <-> E. a e. J z = ( a i^i A ) ) )
31 29 22 30 syl2anc 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> ( z e. ( J |`t A ) <-> E. a e. J z = ( a i^i A ) ) )
32 r19.29 
 |-  ( ( A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) /\ E. a e. J z = ( a i^i A ) ) -> E. a e. J ( ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) /\ z = ( a i^i A ) ) )
33 simprr 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) -> x e. A )
34 33 a1d 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) -> ( x e. y -> x e. A ) )
35 34 ancld 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) -> ( x e. y -> ( x e. y /\ x e. A ) ) )
36 elin 
 |-  ( x e. ( y i^i A ) <-> ( x e. y /\ x e. A ) )
37 35 36 syl6ibr 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) -> ( x e. y -> x e. ( y i^i A ) ) )
38 ssrin 
 |-  ( y C_ a -> ( y i^i A ) C_ ( a i^i A ) )
39 37 38 anim12d1 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) -> ( ( x e. y /\ y C_ a ) -> ( x e. ( y i^i A ) /\ ( y i^i A ) C_ ( a i^i A ) ) ) )
40 39 reximdv 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) -> ( E. y e. t ( x e. y /\ y C_ a ) -> E. y e. t ( x e. ( y i^i A ) /\ ( y i^i A ) C_ ( a i^i A ) ) ) )
41 vex 
 |-  y e. _V
42 41 inex1 
 |-  ( y i^i A ) e. _V
43 42 a1i 
 |-  ( ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) /\ y e. t ) -> ( y i^i A ) e. _V )
44 simp-4r 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) -> A e. V )
45 elrest 
 |-  ( ( t e. _V /\ A e. V ) -> ( w e. ( t |`t A ) <-> E. y e. t w = ( y i^i A ) ) )
46 21 44 45 sylancr 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) -> ( w e. ( t |`t A ) <-> E. y e. t w = ( y i^i A ) ) )
47 eleq2 
 |-  ( w = ( y i^i A ) -> ( x e. w <-> x e. ( y i^i A ) ) )
48 sseq1 
 |-  ( w = ( y i^i A ) -> ( w C_ ( a i^i A ) <-> ( y i^i A ) C_ ( a i^i A ) ) )
49 47 48 anbi12d 
 |-  ( w = ( y i^i A ) -> ( ( x e. w /\ w C_ ( a i^i A ) ) <-> ( x e. ( y i^i A ) /\ ( y i^i A ) C_ ( a i^i A ) ) ) )
50 49 adantl 
 |-  ( ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) /\ w = ( y i^i A ) ) -> ( ( x e. w /\ w C_ ( a i^i A ) ) <-> ( x e. ( y i^i A ) /\ ( y i^i A ) C_ ( a i^i A ) ) ) )
51 43 46 50 rexxfr2d 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) -> ( E. w e. ( t |`t A ) ( x e. w /\ w C_ ( a i^i A ) ) <-> E. y e. t ( x e. ( y i^i A ) /\ ( y i^i A ) C_ ( a i^i A ) ) ) )
52 40 51 sylibrd 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ ( a e. J /\ x e. A ) ) -> ( E. y e. t ( x e. y /\ y C_ a ) -> E. w e. ( t |`t A ) ( x e. w /\ w C_ ( a i^i A ) ) ) )
53 52 expr 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ a e. J ) -> ( x e. A -> ( E. y e. t ( x e. y /\ y C_ a ) -> E. w e. ( t |`t A ) ( x e. w /\ w C_ ( a i^i A ) ) ) ) )
54 53 com23 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ a e. J ) -> ( E. y e. t ( x e. y /\ y C_ a ) -> ( x e. A -> E. w e. ( t |`t A ) ( x e. w /\ w C_ ( a i^i A ) ) ) ) )
55 54 imim2d 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ a e. J ) -> ( ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) -> ( x e. a -> ( x e. A -> E. w e. ( t |`t A ) ( x e. w /\ w C_ ( a i^i A ) ) ) ) ) )
56 55 imp4b 
 |-  ( ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ a e. J ) /\ ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) -> ( ( x e. a /\ x e. A ) -> E. w e. ( t |`t A ) ( x e. w /\ w C_ ( a i^i A ) ) ) )
57 eleq2 
 |-  ( z = ( a i^i A ) -> ( x e. z <-> x e. ( a i^i A ) ) )
58 elin 
 |-  ( x e. ( a i^i A ) <-> ( x e. a /\ x e. A ) )
59 57 58 bitrdi 
 |-  ( z = ( a i^i A ) -> ( x e. z <-> ( x e. a /\ x e. A ) ) )
60 sseq2 
 |-  ( z = ( a i^i A ) -> ( w C_ z <-> w C_ ( a i^i A ) ) )
61 60 anbi2d 
 |-  ( z = ( a i^i A ) -> ( ( x e. w /\ w C_ z ) <-> ( x e. w /\ w C_ ( a i^i A ) ) ) )
62 61 rexbidv 
 |-  ( z = ( a i^i A ) -> ( E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) <-> E. w e. ( t |`t A ) ( x e. w /\ w C_ ( a i^i A ) ) ) )
63 59 62 imbi12d 
 |-  ( z = ( a i^i A ) -> ( ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) <-> ( ( x e. a /\ x e. A ) -> E. w e. ( t |`t A ) ( x e. w /\ w C_ ( a i^i A ) ) ) ) )
64 56 63 syl5ibrcom 
 |-  ( ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ a e. J ) /\ ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) -> ( z = ( a i^i A ) -> ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) )
65 64 expimpd 
 |-  ( ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) /\ a e. J ) -> ( ( ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) /\ z = ( a i^i A ) ) -> ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) )
66 65 rexlimdva 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) -> ( E. a e. J ( ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) /\ z = ( a i^i A ) ) -> ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) )
67 32 66 syl5 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) -> ( ( A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) /\ E. a e. J z = ( a i^i A ) ) -> ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) )
68 67 expd 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ t e. ~P J ) -> ( A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) -> ( E. a e. J z = ( a i^i A ) -> ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) ) )
69 68 impr 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) -> ( E. a e. J z = ( a i^i A ) -> ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) )
70 69 adantrrl 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> ( E. a e. J z = ( a i^i A ) -> ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) )
71 31 70 sylbid 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> ( z e. ( J |`t A ) -> ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) )
72 71 ralrimiv 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> A. z e. ( J |`t A ) ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) )
73 breq1 
 |-  ( y = ( t |`t A ) -> ( y ~<_ _om <-> ( t |`t A ) ~<_ _om ) )
74 rexeq 
 |-  ( y = ( t |`t A ) -> ( E. w e. y ( x e. w /\ w C_ z ) <-> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) )
75 74 imbi2d 
 |-  ( y = ( t |`t A ) -> ( ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) <-> ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) )
76 75 ralbidv 
 |-  ( y = ( t |`t A ) -> ( A. z e. ( J |`t A ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) <-> A. z e. ( J |`t A ) ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) )
77 73 76 anbi12d 
 |-  ( y = ( t |`t A ) -> ( ( y ~<_ _om /\ A. z e. ( J |`t A ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) <-> ( ( t |`t A ) ~<_ _om /\ A. z e. ( J |`t A ) ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) ) )
78 77 rspcev 
 |-  ( ( ( t |`t A ) e. ~P ( J |`t A ) /\ ( ( t |`t A ) ~<_ _om /\ A. z e. ( J |`t A ) ( x e. z -> E. w e. ( t |`t A ) ( x e. w /\ w C_ z ) ) ) ) -> E. y e. ~P ( J |`t A ) ( y ~<_ _om /\ A. z e. ( J |`t A ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
79 20 28 72 78 syl12anc 
 |-  ( ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) /\ ( t e. ~P J /\ ( t ~<_ _om /\ A. a e. J ( x e. a -> E. y e. t ( x e. y /\ y C_ a ) ) ) ) ) -> E. y e. ~P ( J |`t A ) ( y ~<_ _om /\ A. z e. ( J |`t A ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
80 12 79 rexlimddv 
 |-  ( ( ( J e. 1stc /\ A e. V ) /\ x e. ( A i^i U. J ) ) -> E. y e. ~P ( J |`t A ) ( y ~<_ _om /\ A. z e. ( J |`t A ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
81 8 80 syldan 
 |-  ( ( ( J e. 1stc /\ A e. V ) /\ x e. U. ( J |`t A ) ) -> E. y e. ~P ( J |`t A ) ( y ~<_ _om /\ A. z e. ( J |`t A ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
82 81 ralrimiva 
 |-  ( ( J e. 1stc /\ A e. V ) -> A. x e. U. ( J |`t A ) E. y e. ~P ( J |`t A ) ( y ~<_ _om /\ A. z e. ( J |`t A ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) )
83 eqid 
 |-  U. ( J |`t A ) = U. ( J |`t A )
84 83 is1stc2 
 |-  ( ( J |`t A ) e. 1stc <-> ( ( J |`t A ) e. Top /\ A. x e. U. ( J |`t A ) E. y e. ~P ( J |`t A ) ( y ~<_ _om /\ A. z e. ( J |`t A ) ( x e. z -> E. w e. y ( x e. w /\ w C_ z ) ) ) ) )
85 3 82 84 sylanbrc 
 |-  ( ( J e. 1stc /\ A e. V ) -> ( J |`t A ) e. 1stc )