Metamath Proof Explorer


Theorem ptclsg

Description: The closure of a box in the product topology is the box formed from the closures of the factors. The proof uses the axiom of choice; the last hypothesis is the choice assumption. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ptcls.2 J = 𝑡 k A R
ptcls.a φ A V
ptcls.j φ k A R TopOn X
ptcls.c φ k A S X
ptclsg.1 φ k A S AC _ A
Assertion ptclsg φ cls J k A S = k A cls R S

Proof

Step Hyp Ref Expression
1 ptcls.2 J = 𝑡 k A R
2 ptcls.a φ A V
3 ptcls.j φ k A R TopOn X
4 ptcls.c φ k A S X
5 ptclsg.1 φ k A S AC _ A
6 topontop R TopOn X R Top
7 3 6 syl φ k A R Top
8 toponuni R TopOn X X = R
9 3 8 syl φ k A X = R
10 4 9 sseqtrd φ k A S R
11 eqid R = R
12 11 clscld R Top S R cls R S Clsd R
13 7 10 12 syl2anc φ k A cls R S Clsd R
14 2 7 13 ptcldmpt φ k A cls R S Clsd 𝑡 k A R
15 1 fveq2i Clsd J = Clsd 𝑡 k A R
16 14 15 eleqtrrdi φ k A cls R S Clsd J
17 11 sscls R Top S R S cls R S
18 7 10 17 syl2anc φ k A S cls R S
19 18 ralrimiva φ k A S cls R S
20 ss2ixp k A S cls R S k A S k A cls R S
21 19 20 syl φ k A S k A cls R S
22 eqid J = J
23 22 clsss2 k A cls R S Clsd J k A S k A cls R S cls J k A S k A cls R S
24 16 21 23 syl2anc φ cls J k A S k A cls R S
25 vex u V
26 eqeq1 x = u x = y A g y u = y A g y
27 26 anbi2d x = u g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y g Fn A y A g y k A R y z Fin y A z g y = k A R y u = y A g y
28 27 exbidv x = u g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y g g Fn A y A g y k A R y z Fin y A z g y = k A R y u = y A g y
29 25 28 elab u x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y g g Fn A y A g y k A R y z Fin y A z g y = k A R y u = y A g y
30 nffvmpt1 _ k k A R y
31 30 nfel2 k g y k A R y
32 nfv y g k k A R k
33 fveq2 y = k g y = g k
34 fveq2 y = k k A R y = k A R k
35 33 34 eleq12d y = k g y k A R y g k k A R k
36 31 32 35 cbvralw y A g y k A R y k A g k k A R k
37 simpr φ k A k A
38 eqid k A R = k A R
39 38 fvmpt2 k A R TopOn X k A R k = R
40 37 3 39 syl2anc φ k A k A R k = R
41 40 eleq2d φ k A g k k A R k g k R
42 41 ralbidva φ k A g k k A R k k A g k R
43 36 42 syl5bb φ y A g y k A R y k A g k R
44 43 anbi2d φ g Fn A y A g y k A R y g Fn A k A g k R
45 44 adantr φ f k A cls R S g Fn A y A g y k A R y g Fn A k A g k R
46 45 biimpa φ f k A cls R S g Fn A y A g y k A R y g Fn A k A g k R
47 5 ad2antrr φ f k A cls R S g Fn A k A g k R f y A g y k A S AC _ A
48 simpll φ f k A cls R S g Fn A k A g k R f y A g y φ
49 vex f V
50 49 elixp f k A cls R S f Fn A k A f k cls R S
51 50 simprbi f k A cls R S k A f k cls R S
52 51 ad2antlr φ f k A cls R S g Fn A k A g k R f y A g y k A f k cls R S
53 11 clsndisj R Top S R f k cls R S g k R f k g k g k S
54 53 ex R Top S R f k cls R S g k R f k g k g k S
55 54 3expia R Top S R f k cls R S g k R f k g k g k S
56 7 10 55 syl2anc φ k A f k cls R S g k R f k g k g k S
57 56 ralimdva φ k A f k cls R S k A g k R f k g k g k S
58 48 52 57 sylc φ f k A cls R S g Fn A k A g k R f y A g y k A g k R f k g k g k S
59 simprlr φ f k A cls R S g Fn A k A g k R f y A g y k A g k R
60 simprr φ f k A cls R S g Fn A k A g k R f y A g y f y A g y
61 33 cbvixpv y A g y = k A g k
62 60 61 eleqtrdi φ f k A cls R S g Fn A k A g k R f y A g y f k A g k
63 49 elixp f k A g k f Fn A k A f k g k
64 63 simprbi f k A g k k A f k g k
65 62 64 syl φ f k A cls R S g Fn A k A g k R f y A g y k A f k g k
66 r19.26 k A g k R f k g k k A g k R k A f k g k
67 59 65 66 sylanbrc φ f k A cls R S g Fn A k A g k R f y A g y k A g k R f k g k
68 ralim k A g k R f k g k g k S k A g k R f k g k k A g k S
69 58 67 68 sylc φ f k A cls R S g Fn A k A g k R f y A g y k A g k S
70 rabn0 z k A S | z g k S z k A S z g k S
71 dfin5 k A S g k S = z k A S | z g k S
72 inss2 g k S S
73 ssiun2 k A S k A S
74 72 73 sstrid k A g k S k A S
75 sseqin2 g k S k A S k A S g k S = g k S
76 74 75 sylib k A k A S g k S = g k S
77 71 76 eqtr3id k A z k A S | z g k S = g k S
78 77 neeq1d k A z k A S | z g k S g k S
79 70 78 bitr3id k A z k A S z g k S g k S
80 79 ralbiia k A z k A S z g k S k A g k S
81 69 80 sylibr φ f k A cls R S g Fn A k A g k R f y A g y k A z k A S z g k S
82 nfv y z k A S z g k S
83 nfiu1 _ k k A S
84 nfcv _ k g y
85 nfcsb1v _ k y / k S
86 84 85 nfin _ k g y y / k S
87 86 nfel2 k z g y y / k S
88 83 87 nfrex k z k A S z g y y / k S
89 fveq2 k = y g k = g y
90 csbeq1a k = y S = y / k S
91 89 90 ineq12d k = y g k S = g y y / k S
92 91 eleq2d k = y z g k S z g y y / k S
93 92 rexbidv k = y z k A S z g k S z k A S z g y y / k S
94 82 88 93 cbvralw k A z k A S z g k S y A z k A S z g y y / k S
95 81 94 sylib φ f k A cls R S g Fn A k A g k R f y A g y y A z k A S z g y y / k S
96 eleq1 z = h y z g y y / k S h y g y y / k S
97 96 acni3 k A S AC _ A y A z k A S z g y y / k S h h : A k A S y A h y g y y / k S
98 47 95 97 syl2anc φ f k A cls R S g Fn A k A g k R f y A g y h h : A k A S y A h y g y y / k S
99 ffn h : A k A S h Fn A
100 nfv y h k g k S
101 86 nfel2 k h y g y y / k S
102 fveq2 k = y h k = h y
103 102 91 eleq12d k = y h k g k S h y g y y / k S
104 100 101 103 cbvralw k A h k g k S y A h y g y y / k S
105 ne0i h k A g k S k A g k S
106 vex h V
107 106 elixp h k A g k S h Fn A k A h k g k S
108 ixpin k A g k S = k A g k k A S
109 61 ineq1i y A g y k A S = k A g k k A S
110 108 109 eqtr4i k A g k S = y A g y k A S
111 110 neeq1i k A g k S y A g y k A S
112 105 107 111 3imtr3i h Fn A k A h k g k S y A g y k A S
113 104 112 sylan2br h Fn A y A h y g y y / k S y A g y k A S
114 99 113 sylan h : A k A S y A h y g y y / k S y A g y k A S
115 114 exlimiv h h : A k A S y A h y g y y / k S y A g y k A S
116 98 115 syl φ f k A cls R S g Fn A k A g k R f y A g y y A g y k A S
117 116 expr φ f k A cls R S g Fn A k A g k R f y A g y y A g y k A S
118 46 117 syldan φ f k A cls R S g Fn A y A g y k A R y f y A g y y A g y k A S
119 118 3adantr3 φ f k A cls R S g Fn A y A g y k A R y z Fin y A z g y = k A R y f y A g y y A g y k A S
120 eleq2 u = y A g y f u f y A g y
121 ineq1 u = y A g y u k A S = y A g y k A S
122 121 neeq1d u = y A g y u k A S y A g y k A S
123 120 122 imbi12d u = y A g y f u u k A S f y A g y y A g y k A S
124 119 123 syl5ibrcom φ f k A cls R S g Fn A y A g y k A R y z Fin y A z g y = k A R y u = y A g y f u u k A S
125 124 expimpd φ f k A cls R S g Fn A y A g y k A R y z Fin y A z g y = k A R y u = y A g y f u u k A S
126 125 exlimdv φ f k A cls R S g g Fn A y A g y k A R y z Fin y A z g y = k A R y u = y A g y f u u k A S
127 29 126 syl5bi φ f k A cls R S u x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y f u u k A S
128 127 ralrimiv φ f k A cls R S u x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y f u u k A S
129 7 fmpttd φ k A R : A Top
130 129 ffnd φ k A R Fn A
131 eqid x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y = x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y
132 131 ptval A V k A R Fn A 𝑡 k A R = topGen x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y
133 2 130 132 syl2anc φ 𝑡 k A R = topGen x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y
134 1 133 syl5eq φ J = topGen x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y
135 134 adantr φ f k A cls R S J = topGen x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y
136 3 ralrimiva φ k A R TopOn X
137 1 pttopon A V k A R TopOn X J TopOn k A X
138 2 136 137 syl2anc φ J TopOn k A X
139 toponuni J TopOn k A X k A X = J
140 138 139 syl φ k A X = J
141 140 adantr φ f k A cls R S k A X = J
142 131 ptbas A V k A R : A Top x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y TopBases
143 2 129 142 syl2anc φ x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y TopBases
144 143 adantr φ f k A cls R S x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y TopBases
145 4 ralrimiva φ k A S X
146 ss2ixp k A S X k A S k A X
147 145 146 syl φ k A S k A X
148 147 adantr φ f k A cls R S k A S k A X
149 11 clsss3 R Top S R cls R S R
150 7 10 149 syl2anc φ k A cls R S R
151 150 9 sseqtrrd φ k A cls R S X
152 151 ralrimiva φ k A cls R S X
153 ss2ixp k A cls R S X k A cls R S k A X
154 152 153 syl φ k A cls R S k A X
155 154 sselda φ f k A cls R S f k A X
156 135 141 144 148 155 elcls3 φ f k A cls R S f cls J k A S u x | g g Fn A y A g y k A R y z Fin y A z g y = k A R y x = y A g y f u u k A S
157 128 156 mpbird φ f k A cls R S f cls J k A S
158 24 157 eqelssd φ cls J k A S = k A cls R S