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 1 st 𝜔 A V J 𝑡 A 1 st 𝜔

Proof

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