Metamath Proof Explorer

Theorem ptrescn

Description: Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015)

Ref Expression
Hypotheses ptrescn.1 ⊢X=⋃J
ptrescn.2 ⊢J=∏𝑡⁡F
ptrescn.3 ⊢K=∏𝑡⁡F↾B
Assertion ptrescn ⊢A∈V∧F:A⟶Top∧B⊆A→x∈X⟼x↾B∈JCnK

Proof

Step Hyp Ref Expression
1 ptrescn.1 ⊢X=⋃J
2 ptrescn.2 ⊢J=∏𝑡⁡F
3 ptrescn.3 ⊢K=∏𝑡⁡F↾B
4 simpl3 ⊢A∈V∧F:A⟶Top∧B⊆A∧x∈X→B⊆A
5 2 ptuni ⊢A∈V∧F:A⟶Top→⨉k∈A⋃F⁡k=⋃J
6 5 3adant3 ⊢A∈V∧F:A⟶Top∧B⊆A→⨉k∈A⋃F⁡k=⋃J
7 6 1 eqtr4di ⊢A∈V∧F:A⟶Top∧B⊆A→⨉k∈A⋃F⁡k=X
8 7 eleq2d ⊢A∈V∧F:A⟶Top∧B⊆A→x∈⨉k∈A⋃F⁡k↔x∈X
9 8 biimpar ⊢A∈V∧F:A⟶Top∧B⊆A∧x∈X→x∈⨉k∈A⋃F⁡k
10 resixp ⊢B⊆A∧x∈⨉k∈A⋃F⁡k→x↾B∈⨉k∈B⋃F⁡k
11 4 9 10 syl2anc ⊢A∈V∧F:A⟶Top∧B⊆A∧x∈X→x↾B∈⨉k∈B⋃F⁡k
12 ixpeq2 ⊢∀k∈B⋃F↾B⁡k=⋃F⁡k→⨉k∈B⋃F↾B⁡k=⨉k∈B⋃F⁡k
13 fvres ⊢k∈B→F↾B⁡k=F⁡k
14 13 unieqd ⊢k∈B→⋃F↾B⁡k=⋃F⁡k
15 12 14 mprg ⊢⨉k∈B⋃F↾B⁡k=⨉k∈B⋃F⁡k
16 ssexg ⊢B⊆A∧A∈V→B∈V
17 16 ancoms ⊢A∈V∧B⊆A→B∈V
18 17 3adant2 ⊢A∈V∧F:A⟶Top∧B⊆A→B∈V
19 fssres ⊢F:A⟶Top∧B⊆A→F↾B:B⟶Top
20 19 3adant1 ⊢A∈V∧F:A⟶Top∧B⊆A→F↾B:B⟶Top
21 3 ptuni ⊢B∈V∧F↾B:B⟶Top→⨉k∈B⋃F↾B⁡k=⋃K
22 18 20 21 syl2anc ⊢A∈V∧F:A⟶Top∧B⊆A→⨉k∈B⋃F↾B⁡k=⋃K
23 15 22 eqtr3id ⊢A∈V∧F:A⟶Top∧B⊆A→⨉k∈B⋃F⁡k=⋃K
24 23 adantr ⊢A∈V∧F:A⟶Top∧B⊆A∧x∈X→⨉k∈B⋃F⁡k=⋃K
25 11 24 eleqtrd ⊢A∈V∧F:A⟶Top∧B⊆A∧x∈X→x↾B∈⋃K
26 25 fmpttd ⊢A∈V∧F:A⟶Top∧B⊆A→x∈X⟼x↾B:X⟶⋃K
27 fimacnv ⊢x∈X⟼x↾B:X⟶⋃K→x∈X⟼x↾B-1⋃K=X
28 26 27 syl ⊢A∈V∧F:A⟶Top∧B⊆A→x∈X⟼x↾B-1⋃K=X
29 pttop ⊢A∈V∧F:A⟶Top→∏𝑡⁡F∈Top
30 2 29 eqeltrid ⊢A∈V∧F:A⟶Top→J∈Top
31 30 3adant3 ⊢A∈V∧F:A⟶Top∧B⊆A→J∈Top
32 1 topopn ⊢J∈Top→X∈J
33 31 32 syl ⊢A∈V∧F:A⟶Top∧B⊆A→X∈J
34 28 33 eqeltrd ⊢A∈V∧F:A⟶Top∧B⊆A→x∈X⟼x↾B-1⋃K∈J
35 elsni ⊢v∈⋃K→v=⋃K
36 35 imaeq2d ⊢v∈⋃K→x∈X⟼x↾B-1v=x∈X⟼x↾B-1⋃K
37 36 eleq1d ⊢v∈⋃K→x∈X⟼x↾B-1v∈J↔x∈X⟼x↾B-1⋃K∈J
38 34 37 syl5ibrcom ⊢A∈V∧F:A⟶Top∧B⊆A→v∈⋃K→x∈X⟼x↾B-1v∈J
39 38 ralrimiv ⊢A∈V∧F:A⟶Top∧B⊆A→∀v∈⋃Kx∈X⟼x↾B-1v∈J
40 imaco ⊢x∈X⟼x↾B-1∘z∈⋃K⟼z⁡k-1u=x∈X⟼x↾B-1z∈⋃K⟼z⁡k-1u
41 cnvco ⊢z∈⋃K⟼z⁡k∘x∈X⟼x↾B-1=x∈X⟼x↾B-1∘z∈⋃K⟼z⁡k-1
42 25 adantlr ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k∧x∈X→x↾B∈⋃K
43 eqidd ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→x∈X⟼x↾B=x∈X⟼x↾B
44 eqidd ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→z∈⋃K⟼z⁡k=z∈⋃K⟼z⁡k
45 fveq1 ⊢z=x↾B→z⁡k=x↾B⁡k
46 42 43 44 45 fmptco ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→z∈⋃K⟼z⁡k∘x∈X⟼x↾B=x∈X⟼x↾B⁡k
47 fvres ⊢k∈B→x↾B⁡k=x⁡k
48 47 ad2antrl ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→x↾B⁡k=x⁡k
49 48 mpteq2dv ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→x∈X⟼x↾B⁡k=x∈X⟼x⁡k
50 46 49 eqtrd ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→z∈⋃K⟼z⁡k∘x∈X⟼x↾B=x∈X⟼x⁡k
51 50 cnveqd ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→z∈⋃K⟼z⁡k∘x∈X⟼x↾B-1=x∈X⟼x⁡k-1
52 41 51 eqtr3id ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→x∈X⟼x↾B-1∘z∈⋃K⟼z⁡k-1=x∈X⟼x⁡k-1
53 52 imaeq1d ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→x∈X⟼x↾B-1∘z∈⋃K⟼z⁡k-1u=x∈X⟼x⁡k-1u
54 40 53 eqtr3id ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→x∈X⟼x↾B-1z∈⋃K⟼z⁡k-1u=x∈X⟼x⁡k-1u
55 simpl1 ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→A∈V
56 simpl2 ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→F:A⟶Top
57 simpl3 ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→B⊆A
58 simprl ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→k∈B
59 57 58 sseldd ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→k∈A
60 1 2 ptpjcn ⊢A∈V∧F:A⟶Top∧k∈A→x∈X⟼x⁡k∈JCnF⁡k
61 55 56 59 60 syl3anc ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→x∈X⟼x⁡k∈JCnF⁡k
62 simprr ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→u∈F⁡k
63 cnima ⊢x∈X⟼x⁡k∈JCnF⁡k∧u∈F⁡k→x∈X⟼x⁡k-1u∈J
64 61 62 63 syl2anc ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→x∈X⟼x⁡k-1u∈J
65 54 64 eqeltrd ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→x∈X⟼x↾B-1z∈⋃K⟼z⁡k-1u∈J
66 imaeq2 ⊢v=z∈⋃K⟼z⁡k-1u→x∈X⟼x↾B-1v=x∈X⟼x↾B-1z∈⋃K⟼z⁡k-1u
67 66 eleq1d ⊢v=z∈⋃K⟼z⁡k-1u→x∈X⟼x↾B-1v∈J↔x∈X⟼x↾B-1z∈⋃K⟼z⁡k-1u∈J
68 65 67 syl5ibrcom ⊢A∈V∧F:A⟶Top∧B⊆A∧k∈B∧u∈F⁡k→v=z∈⋃K⟼z⁡k-1u→x∈X⟼x↾B-1v∈J
69 68 rexlimdvva ⊢A∈V∧F:A⟶Top∧B⊆A→∃k∈B∃u∈F⁡kv=z∈⋃K⟼z⁡k-1u→x∈X⟼x↾B-1v∈J
70 69 alrimiv ⊢A∈V∧F:A⟶Top∧B⊆A→∀v∃k∈B∃u∈F⁡kv=z∈⋃K⟼z⁡k-1u→x∈X⟼x↾B-1v∈J
71 eqid ⊢k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1u=k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1u
72 71 rnmpo ⊢ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1u=y|∃k∈B∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1u
73 72 raleqi ⊢∀v∈ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1ux∈X⟼x↾B-1v∈J↔∀v∈y|∃k∈B∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1ux∈X⟼x↾B-1v∈J
74 13 rexeqdv ⊢k∈B→∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1u↔∃u∈F⁡ky=z∈⋃K⟼z⁡k-1u
75 eqeq1 ⊢y=v→y=z∈⋃K⟼z⁡k-1u↔v=z∈⋃K⟼z⁡k-1u
76 75 rexbidv ⊢y=v→∃u∈F⁡ky=z∈⋃K⟼z⁡k-1u↔∃u∈F⁡kv=z∈⋃K⟼z⁡k-1u
77 74 76 sylan9bbr ⊢y=v∧k∈B→∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1u↔∃u∈F⁡kv=z∈⋃K⟼z⁡k-1u
78 77 rexbidva ⊢y=v→∃k∈B∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1u↔∃k∈B∃u∈F⁡kv=z∈⋃K⟼z⁡k-1u
79 78 ralab ⊢∀v∈y|∃k∈B∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1ux∈X⟼x↾B-1v∈J↔∀v∃k∈B∃u∈F⁡kv=z∈⋃K⟼z⁡k-1u→x∈X⟼x↾B-1v∈J
80 73 79 bitri ⊢∀v∈ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1ux∈X⟼x↾B-1v∈J↔∀v∃k∈B∃u∈F⁡kv=z∈⋃K⟼z⁡k-1u→x∈X⟼x↾B-1v∈J
81 70 80 sylibr ⊢A∈V∧F:A⟶Top∧B⊆A→∀v∈ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1ux∈X⟼x↾B-1v∈J
82 ralunb ⊢∀v∈⋃K∪ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1ux∈X⟼x↾B-1v∈J↔∀v∈⋃Kx∈X⟼x↾B-1v∈J∧∀v∈ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1ux∈X⟼x↾B-1v∈J
83 39 81 82 sylanbrc ⊢A∈V∧F:A⟶Top∧B⊆A→∀v∈⋃K∪ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1ux∈X⟼x↾B-1v∈J
84 1 toptopon ⊢J∈Top↔J∈TopOn⁡X
85 31 84 sylib ⊢A∈V∧F:A⟶Top∧B⊆A→J∈TopOn⁡X
86 snex ⊢⋃K∈V
87 fvex ⊢F↾B⁡k∈V
88 87 abrexex ⊢y|∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1u∈V
89 88 rgenw ⊢∀k∈By|∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1u∈V
90 abrexex2g ⊢B∈V∧∀k∈By|∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1u∈V→y|∃k∈B∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1u∈V
91 18 89 90 sylancl ⊢A∈V∧F:A⟶Top∧B⊆A→y|∃k∈B∃u∈F↾B⁡ky=z∈⋃K⟼z⁡k-1u∈V
92 72 91 eqeltrid ⊢A∈V∧F:A⟶Top∧B⊆A→ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1u∈V
93 unexg ⊢⋃K∈V∧ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1u∈V→⋃K∪ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1u∈V
94 86 92 93 sylancr ⊢A∈V∧F:A⟶Top∧B⊆A→⋃K∪ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1u∈V
95 eqid ⊢⋃K=⋃K
96 3 95 71 ptval2 ⊢B∈V∧F↾B:B⟶Top→K=topGen⁡fi⁡⋃K∪ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1u
97 18 20 96 syl2anc ⊢A∈V∧F:A⟶Top∧B⊆A→K=topGen⁡fi⁡⋃K∪ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1u
98 pttop ⊢B∈V∧F↾B:B⟶Top→∏𝑡⁡F↾B∈Top
99 18 20 98 syl2anc ⊢A∈V∧F:A⟶Top∧B⊆A→∏𝑡⁡F↾B∈Top
100 3 99 eqeltrid ⊢A∈V∧F:A⟶Top∧B⊆A→K∈Top
101 95 toptopon ⊢K∈Top↔K∈TopOn⁡⋃K
102 100 101 sylib ⊢A∈V∧F:A⟶Top∧B⊆A→K∈TopOn⁡⋃K
103 85 94 97 102 subbascn ⊢A∈V∧F:A⟶Top∧B⊆A→x∈X⟼x↾B∈JCnK↔x∈X⟼x↾B:X⟶⋃K∧∀v∈⋃K∪ran⁡k∈B,u∈F↾B⁡k⟼z∈⋃K⟼z⁡k-1ux∈X⟼x↾B-1v∈J
104 26 83 103 mpbir2and ⊢A∈V∧F:A⟶Top∧B⊆A→x∈X⟼x↾B∈JCnK