Metamath Proof Explorer

Theorem cnprest2

Description: Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses cnprest.1 ⊢X=⋃J
cnprest.2 ⊢Y=⋃K
Assertion cnprest2 ⊢K∈Top∧F:X⟶B∧B⊆Y→F∈JCnPK⁡P↔F∈JCnPK↾𝑡B⁡P

Proof

Step Hyp Ref Expression
1 cnprest.1 ⊢X=⋃J
2 cnprest.2 ⊢Y=⋃K
3 cnptop1 ⊢F∈JCnPK⁡P→J∈Top
4 1 cnprcl ⊢F∈JCnPK⁡P→P∈X
5 3 4 jca ⊢F∈JCnPK⁡P→J∈Top∧P∈X
6 5 a1i ⊢K∈Top∧F:X⟶B∧B⊆Y→F∈JCnPK⁡P→J∈Top∧P∈X
7 cnptop1 ⊢F∈JCnPK↾𝑡B⁡P→J∈Top
8 1 cnprcl ⊢F∈JCnPK↾𝑡B⁡P→P∈X
9 7 8 jca ⊢F∈JCnPK↾𝑡B⁡P→J∈Top∧P∈X
10 9 a1i ⊢K∈Top∧F:X⟶B∧B⊆Y→F∈JCnPK↾𝑡B⁡P→J∈Top∧P∈X
11 simpl2 ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F:X⟶B
12 simprr ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→P∈X
13 11 12 ffvelcdmd ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F⁡P∈B
14 13 biantrud ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F⁡P∈x↔F⁡P∈x∧F⁡P∈B
15 elin ⊢F⁡P∈x∩B↔F⁡P∈x∧F⁡P∈B
16 14 15 bitr4di ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F⁡P∈x↔F⁡P∈x∩B
17 imassrn ⊢Fy⊆ran⁡F
18 11 frnd ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→ran⁡F⊆B
19 17 18 sstrid ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→Fy⊆B
20 19 biantrud ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→Fy⊆x↔Fy⊆x∧Fy⊆B
21 ssin ⊢Fy⊆x∧Fy⊆B↔Fy⊆x∩B
22 20 21 bitrdi ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→Fy⊆x↔Fy⊆x∩B
23 22 anbi2d ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→P∈y∧Fy⊆x↔P∈y∧Fy⊆x∩B
24 23 rexbidv ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→∃y∈JP∈y∧Fy⊆x↔∃y∈JP∈y∧Fy⊆x∩B
25 16 24 imbi12d ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F⁡P∈x→∃y∈JP∈y∧Fy⊆x↔F⁡P∈x∩B→∃y∈JP∈y∧Fy⊆x∩B
26 25 ralbidv ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→∀x∈KF⁡P∈x→∃y∈JP∈y∧Fy⊆x↔∀x∈KF⁡P∈x∩B→∃y∈JP∈y∧Fy⊆x∩B
27 vex ⊢x∈V
28 27 inex1 ⊢x∩B∈V
29 28 a1i ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X∧x∈K→x∩B∈V
30 simpl1 ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→K∈Top
31 uniexg ⊢K∈Top→⋃K∈V
32 2 31 eqeltrid ⊢K∈Top→Y∈V
33 30 32 syl ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→Y∈V
34 simpl3 ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→B⊆Y
35 33 34 ssexd ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→B∈V
36 elrest ⊢K∈Top∧B∈V→z∈K↾𝑡B↔∃x∈Kz=x∩B
37 30 35 36 syl2anc ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→z∈K↾𝑡B↔∃x∈Kz=x∩B
38 eleq2 ⊢z=x∩B→F⁡P∈z↔F⁡P∈x∩B
39 sseq2 ⊢z=x∩B→Fy⊆z↔Fy⊆x∩B
40 39 anbi2d ⊢z=x∩B→P∈y∧Fy⊆z↔P∈y∧Fy⊆x∩B
41 40 rexbidv ⊢z=x∩B→∃y∈JP∈y∧Fy⊆z↔∃y∈JP∈y∧Fy⊆x∩B
42 38 41 imbi12d ⊢z=x∩B→F⁡P∈z→∃y∈JP∈y∧Fy⊆z↔F⁡P∈x∩B→∃y∈JP∈y∧Fy⊆x∩B
43 42 adantl ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X∧z=x∩B→F⁡P∈z→∃y∈JP∈y∧Fy⊆z↔F⁡P∈x∩B→∃y∈JP∈y∧Fy⊆x∩B
44 29 37 43 ralxfr2d ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→∀z∈K↾𝑡BF⁡P∈z→∃y∈JP∈y∧Fy⊆z↔∀x∈KF⁡P∈x∩B→∃y∈JP∈y∧Fy⊆x∩B
45 26 44 bitr4d ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→∀x∈KF⁡P∈x→∃y∈JP∈y∧Fy⊆x↔∀z∈K↾𝑡BF⁡P∈z→∃y∈JP∈y∧Fy⊆z
46 11 34 fssd ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F:X⟶Y
47 simprl ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→J∈Top
48 1 2 iscnp2 ⊢F∈JCnPK⁡P↔J∈Top∧K∈Top∧P∈X∧F:X⟶Y∧∀x∈KF⁡P∈x→∃y∈JP∈y∧Fy⊆x
49 48 baib ⊢J∈Top∧K∈Top∧P∈X→F∈JCnPK⁡P↔F:X⟶Y∧∀x∈KF⁡P∈x→∃y∈JP∈y∧Fy⊆x
50 47 30 12 49 syl3anc ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F∈JCnPK⁡P↔F:X⟶Y∧∀x∈KF⁡P∈x→∃y∈JP∈y∧Fy⊆x
51 46 50 mpbirand ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F∈JCnPK⁡P↔∀x∈KF⁡P∈x→∃y∈JP∈y∧Fy⊆x
52 1 toptopon ⊢J∈Top↔J∈TopOn⁡X
53 47 52 sylib ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→J∈TopOn⁡X
54 2 toptopon ⊢K∈Top↔K∈TopOn⁡Y
55 30 54 sylib ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→K∈TopOn⁡Y
56 resttopon ⊢K∈TopOn⁡Y∧B⊆Y→K↾𝑡B∈TopOn⁡B
57 55 34 56 syl2anc ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→K↾𝑡B∈TopOn⁡B
58 iscnp ⊢J∈TopOn⁡X∧K↾𝑡B∈TopOn⁡B∧P∈X→F∈JCnPK↾𝑡B⁡P↔F:X⟶B∧∀z∈K↾𝑡BF⁡P∈z→∃y∈JP∈y∧Fy⊆z
59 53 57 12 58 syl3anc ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F∈JCnPK↾𝑡B⁡P↔F:X⟶B∧∀z∈K↾𝑡BF⁡P∈z→∃y∈JP∈y∧Fy⊆z
60 11 59 mpbirand ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F∈JCnPK↾𝑡B⁡P↔∀z∈K↾𝑡BF⁡P∈z→∃y∈JP∈y∧Fy⊆z
61 45 51 60 3bitr4d ⊢K∈Top∧F:X⟶B∧B⊆Y∧J∈Top∧P∈X→F∈JCnPK⁡P↔F∈JCnPK↾𝑡B⁡P
62 61 ex ⊢K∈Top∧F:X⟶B∧B⊆Y→J∈Top∧P∈X→F∈JCnPK⁡P↔F∈JCnPK↾𝑡B⁡P
63 6 10 62 pm5.21ndd ⊢K∈Top∧F:X⟶B∧B⊆Y→F∈JCnPK⁡P↔F∈JCnPK↾𝑡B⁡P