Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  txcnp Unicode version

Theorem txcnp 17314
 Description: If two functions are continuous at , then the ordered pair of them is continuous at into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
txcnp.4 TopOn
txcnp.5 TopOn
txcnp.6 TopOn
txcnp.7
txcnp.8
txcnp.9
Assertion
Ref Expression
txcnp
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()

Proof of Theorem txcnp
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 txcnp.4 . . . . . . 7 TopOn
2 txcnp.5 . . . . . . 7 TopOn
3 txcnp.8 . . . . . . 7
4 cnpf2 16980 . . . . . . 7 TopOn TopOn
51, 2, 3, 4syl3anc 1182 . . . . . 6
6 eqid 2283 . . . . . . 7
76fmpt 5681 . . . . . 6
85, 7sylibr 203 . . . . 5
98r19.21bi 2641 . . . 4
10 txcnp.6 . . . . . . 7 TopOn
11 txcnp.9 . . . . . . 7
12 cnpf2 16980 . . . . . . 7 TopOn TopOn
131, 10, 11, 12syl3anc 1182 . . . . . 6
14 eqid 2283 . . . . . . 7
1514fmpt 5681 . . . . . 6
1613, 15sylibr 203 . . . . 5
1716r19.21bi 2641 . . . 4
18 opelxpi 4721 . . . 4
199, 17, 18syl2anc 642 . . 3
20 eqid 2283 . . 3
2119, 20fmptd 5684 . 2
22 txcnp.7 . . . . . . . . 9
23 simpr 447 . . . . . . . . . . . 12
24 opex 4237 . . . . . . . . . . . 12
2520fvmpt2 5608 . . . . . . . . . . . 12
2623, 24, 25sylancl 643 . . . . . . . . . . 11
276fvmpt2 5608 . . . . . . . . . . . . 13
2823, 9, 27syl2anc 642 . . . . . . . . . . . 12
2914fvmpt2 5608 . . . . . . . . . . . . 13
3023, 17, 29syl2anc 642 . . . . . . . . . . . 12
3128, 30opeq12d 3804 . . . . . . . . . . 11
3226, 31eqtr4d 2318 . . . . . . . . . 10
3332ralrimiva 2626 . . . . . . . . 9
34 nfmpt1 4109 . . . . . . . . . . . 12
35 nfcv 2419 . . . . . . . . . . . 12
3634, 35nffv 5532 . . . . . . . . . . 11
37 nfmpt1 4109 . . . . . . . . . . . . 13
3837, 35nffv 5532 . . . . . . . . . . . 12
39 nfmpt1 4109 . . . . . . . . . . . . 13
4039, 35nffv 5532 . . . . . . . . . . . 12
4138, 40nfop 3812 . . . . . . . . . . 11
4236, 41nfeq 2426 . . . . . . . . . 10
43 fveq2 5525 . . . . . . . . . . 11
44 fveq2 5525 . . . . . . . . . . . 12
45 fveq2 5525 . . . . . . . . . . . 12
4644, 45opeq12d 3804 . . . . . . . . . . 11
4743, 46eqeq12d 2297 . . . . . . . . . 10
4842, 47rspc 2878 . . . . . . . . 9
4922, 33, 48sylc 56 . . . . . . . 8
5049eleq1d 2349 . . . . . . 7
5150adantr 451 . . . . . 6
523ad2antrr 706 . . . . . . . . . 10
53 simplrl 736 . . . . . . . . . 10
54 simprl 732 . . . . . . . . . 10
55 cnpimaex 16986 . . . . . . . . . 10
5652, 53, 54, 55syl3anc 1182 . . . . . . . . 9
5711ad2antrr 706 . . . . . . . . . 10
58 simplrr 737 . . . . . . . . . 10
59 simprr 733 . . . . . . . . . 10
60 cnpimaex 16986 . . . . . . . . . 10
6157, 58, 59, 60syl3anc 1182 . . . . . . . . 9
6256, 61jca 518 . . . . . . . 8
6362ex 423 . . . . . . 7
64 opelxp 4719 . . . . . . 7
65 reeanv 2707 . . . . . . 7
6663, 64, 653imtr4g 261 . . . . . 6
6751, 66sylbid 206 . . . . 5
68 an4 797 . . . . . . . . . . 11
69 elin 3358 . . . . . . . . . . . . . 14
7069biimpri 197 . . . . . . . . . . . . 13
7170a1i 10 . . . . . . . . . . . 12
72 simpl 443 . . . . . . . . . . . . . . . 16
73 toponss 16667 . . . . . . . . . . . . . . . 16 TopOn
741, 72, 73syl2an 463 . . . . . . . . . . . . . . 15
75 ssinss1 3397 . . . . . . . . . . . . . . . . . . . . 21
7675adantl 452 . . . . . . . . . . . . . . . . . . . 20
7776sselda 3180 . . . . . . . . . . . . . . . . . . 19
7833ad2antrr 706 . . . . . . . . . . . . . . . . . . 19
79 nfcv 2419 . . . . . . . . . . . . . . . . . . . . . 22
8034, 79nffv 5532 . . . . . . . . . . . . . . . . . . . . 21
8137, 79nffv 5532 . . . . . . . . . . . . . . . . . . . . . 22
8239, 79nffv 5532 . . . . . . . . . . . . . . . . . . . . . 22
8381, 82nfop 3812 . . . . . . . . . . . . . . . . . . . . 21
8480, 83nfeq 2426 . . . . . . . . . . . . . . . . . . . 20
85 fveq2 5525 . . . . . . . . . . . . . . . . . . . . 21
86 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . 22
87 fveq2 5525 . . . . . . . . . . . . . . . . . . . . . 22
8886, 87opeq12d 3804 . . . . . . . . . . . . . . . . . . . . 21
8985, 88eqeq12d 2297 . . . . . . . . . . . . . . . . . . . 20
9084, 89rspc 2878 . . . . . . . . . . . . . . . . . . 19
9177, 78, 90sylc 56 . . . . . . . . . . . . . . . . . 18
92 inss1 3389 . . . . . . . . . . . . . . . . . . . . 21
93 simpr 447 . . . . . . . . . . . . . . . . . . . . 21
9492, 93sseldi 3178 . . . . . . . . . . . . . . . . . . . 20
955ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22
96 ffun 5391 . . . . . . . . . . . . . . . . . . . . . 22
9795, 96syl 15 . . . . . . . . . . . . . . . . . . . . 21
9876adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23
99 fdm 5393 . . . . . . . . . . . . . . . . . . . . . . . 24
10095, 99syl 15 . . . . . . . . . . . . . . . . . . . . . . 23
10198, 100sseqtr4d 3215 . . . . . . . . . . . . . . . . . . . . . 22
102101, 93sseldd 3181 . . . . . . . . . . . . . . . . . . . . 21
103 funfvima 5753 . . . . . . . . . . . . . . . . . . . . 21
10497, 102, 103syl2anc 642 . . . . . . . . . . . . . . . . . . . 20
10594, 104mpd 14 . . . . . . . . . . . . . . . . . . 19
106 inss2 3390 . . . . . . . . . . . . . . . . . . . . 21
107106, 93sseldi 3178 . . . . . . . . . . . . . . . . . . . 20
10813ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22
109 ffun 5391 . . . . . . . . . . . . . . . . . . . . . 22
110108, 109syl 15 . . . . . . . . . . . . . . . . . . . . 21
111 fdm 5393 . . . . . . . . . . . . . . . . . . . . . . . 24
112108, 111syl 15 . . . . . . . . . . . . . . . . . . . . . . 23
11398, 112sseqtr4d 3215 . . . . . . . . . . . . . . . . . . . . . 22
114113, 93sseldd 3181 . . . . . . . . . . . . . . . . . . . . 21
115 funfvima 5753 . . . . . . . . . . . . . . . . . . . . 21
116110, 114, 115syl2anc 642 . . . . . . . . . . . . . . . . . . . 20
117107, 116mpd 14 . . . . . . . . . . . . . . . . . . 19
118 opelxpi 4721 . . . . . . . . . . . . . . . . . . 19
119105, 117, 118syl2anc 642 . . . . . . . . . . . . . . . . . 18
12091, 119eqeltrd 2357 . . . . . . . . . . . . . . . . 17
121120ralrimiva 2626 . . . . . . . . . . . . . . . 16
122 ffun 5391 . . . . . . . . . . . . . . . . . . 19
12321, 122syl 15 . . . . . . . . . . . . . . . . . 18
124123adantr 451 . . . . . . . . . . . . . . . . 17
125 fdm 5393 . . . . . . . . . . . . . . . . . . . 20
12621, 125syl 15 . . . . . . . . . . . . . . . . . . 19
127126adantr 451 . . . . . . . . . . . . . . . . . 18
12876, 127sseqtr4d 3215 . . . . . . . . . . . . . . . . 17
129 funimass4 5573 . . . . . . . . . . . . . . . . 17
130124, 128, 129syl2anc 642 . . . . . . . . . . . . . . . 16
131121, 130mpbird 223 . . . . . . . . . . . . . . 15
13274, 131syldan 456 . . . . . . . . . . . . . 14
133132adantlr 695 . . . . . . . . . . . . 13
134 xpss12 4792 . . . . . . . . . . . . 13
135 sstr2 3186 . . . . . . . . . . . . 13
136133, 134, 135syl2im 34 . . . . . . . . . . . 12
13771, 136anim12d 546 . . . . . . . . . . 11
13868, 137syl5bi 208 . . . . . . . . . 10
139 topontop 16664 . . . . . . . . . . . . 13 TopOn
1401, 139syl 15 . . . . . . . . . . . 12
141 inopn 16645 . . . . . . . . . . . . 13
1421413expb 1152 . . . . . . . . . . . 12
143140, 142sylan 457 . . . . . . . . . . 11
144143adantlr 695 . . . . . . . . . 10
145138, 144jctild 527 . . . . . . . . 9
146145expimpd 586 . . . . . . . 8
147 eleq2 2344 . . . . . . . . . 10
148 imaeq2 5008 . . . . . . . . . . 11
149148sseq1d 3205 . . . . . . . . . 10
150147, 149anbi12d 691 . . . . . . . . 9
151150rspcev 2884 . . . . . . . 8
152146, 151syl6 29 . . . . . . 7
153152exp3a 425 . . . . . 6
154153rexlimdvv 2673 . . . . 5
15567, 154syld 40 . . . 4
156155ralrimivva 2635 . . 3
157 vex 2791 . . . . . 6
158 vex 2791 . . . . . 6
159157, 158xpex 4801 . . . . 5
160159rgen2w 2611 . . . 4
161 eqid 2283 . . . . 5
162 eleq2 2344 . . . . . 6
163 sseq2 3200 . . . . . . . 8
164163anbi2d 684 . . . . . . 7
165164rexbidv 2564 . . . . . 6
166162, 165imbi12d 311 . . . . 5
167161, 166ralrnmpt2 5958 . . . 4
168160, 167ax-mp 8 . . 3
169156, 168sylibr 203 . 2
170 topontop 16664 . . . . 5 TopOn
1712, 170syl 15 . . . 4
172 topontop 16664 . . . . 5 TopOn
17310, 172syl 15 . . . 4
174 eqid 2283 . . . . 5
175174txval 17259 . . . 4
176171, 173, 175syl2anc 642 . . 3
177 txtopon 17286 . . . 4 TopOn TopOn TopOn
1782, 10, 177syl2anc 642 . . 3 TopOn
1791, 176, 178, 22tgcnp 16983 . 2
18021, 169, 179mpbir2and 888 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   wceq 1623   wcel 1684  wral 2543  wrex 2544  cvv 2788   cin 3151   wss 3152  cop 3643   cmpt 4077   cxp 4687   cdm 4689   crn 4690  cima 4692   wfun 5249  wf 5251  cfv 5255  (class class class)co 5858   cmpt2 5860  ctg 13342  ctop 16631  TopOnctopon 16632   ccnp 16955   ctx 17255 This theorem is referenced by:  limccnp2  19242 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-map 6774  df-topgen 13344  df-top 16636  df-bases 16638  df-topon 16639  df-cnp 16958  df-tx 17257
 Copyright terms: Public domain W3C validator