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

Theorem txcnp 20635
 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 20266 . . . . . . 7 TopOn TopOn
51, 2, 3, 4syl3anc 1268 . . . . . 6
6 eqid 2451 . . . . . . 7
76fmpt 6043 . . . . . 6
85, 7sylibr 216 . . . . 5
98r19.21bi 2757 . . . 4
10 txcnp.6 . . . . . . 7 TopOn
11 txcnp.9 . . . . . . 7
12 cnpf2 20266 . . . . . . 7 TopOn TopOn
131, 10, 11, 12syl3anc 1268 . . . . . 6
14 eqid 2451 . . . . . . 7
1514fmpt 6043 . . . . . 6
1613, 15sylibr 216 . . . . 5
1716r19.21bi 2757 . . . 4
18 opelxpi 4866 . . . 4
199, 17, 18syl2anc 667 . . 3
20 eqid 2451 . . 3
2119, 20fmptd 6046 . 2
22 txcnp.7 . . . . . . . . 9
23 simpr 463 . . . . . . . . . . . 12
24 opex 4664 . . . . . . . . . . . 12
2520fvmpt2 5957 . . . . . . . . . . . 12
2623, 24, 25sylancl 668 . . . . . . . . . . 11
276fvmpt2 5957 . . . . . . . . . . . . 13
2823, 9, 27syl2anc 667 . . . . . . . . . . . 12
2914fvmpt2 5957 . . . . . . . . . . . . 13
3023, 17, 29syl2anc 667 . . . . . . . . . . . 12
3128, 30opeq12d 4174 . . . . . . . . . . 11
3226, 31eqtr4d 2488 . . . . . . . . . 10
3332ralrimiva 2802 . . . . . . . . 9
34 nffvmpt1 5873 . . . . . . . . . . 11
35 nffvmpt1 5873 . . . . . . . . . . . 12
36 nffvmpt1 5873 . . . . . . . . . . . 12
3735, 36nfop 4182 . . . . . . . . . . 11
3834, 37nfeq 2603 . . . . . . . . . 10
39 fveq2 5865 . . . . . . . . . . 11
40 fveq2 5865 . . . . . . . . . . . 12
41 fveq2 5865 . . . . . . . . . . . 12
4240, 41opeq12d 4174 . . . . . . . . . . 11
4339, 42eqeq12d 2466 . . . . . . . . . 10
4438, 43rspc 3144 . . . . . . . . 9
4522, 33, 44sylc 62 . . . . . . . 8
4645eleq1d 2513 . . . . . . 7
4746adantr 467 . . . . . 6
483ad2antrr 732 . . . . . . . . . 10
49 simplrl 770 . . . . . . . . . 10
50 simprl 764 . . . . . . . . . 10
51 cnpimaex 20272 . . . . . . . . . 10
5248, 49, 50, 51syl3anc 1268 . . . . . . . . 9
5311ad2antrr 732 . . . . . . . . . 10
54 simplrr 771 . . . . . . . . . 10
55 simprr 766 . . . . . . . . . 10
56 cnpimaex 20272 . . . . . . . . . 10
5753, 54, 55, 56syl3anc 1268 . . . . . . . . 9
5852, 57jca 535 . . . . . . . 8
5958ex 436 . . . . . . 7
60 opelxp 4864 . . . . . . 7
61 reeanv 2958 . . . . . . 7
6259, 60, 613imtr4g 274 . . . . . 6
6347, 62sylbid 219 . . . . 5
64 an4 833 . . . . . . . . . . 11
65 elin 3617 . . . . . . . . . . . . . 14
6665biimpri 210 . . . . . . . . . . . . 13
6766a1i 11 . . . . . . . . . . . 12
68 simpl 459 . . . . . . . . . . . . . . . 16
69 toponss 19944 . . . . . . . . . . . . . . . 16 TopOn
701, 68, 69syl2an 480 . . . . . . . . . . . . . . 15
71 ssinss1 3660 . . . . . . . . . . . . . . . . . . . . 21
7271adantl 468 . . . . . . . . . . . . . . . . . . . 20
7372sselda 3432 . . . . . . . . . . . . . . . . . . 19
7433ad2antrr 732 . . . . . . . . . . . . . . . . . . 19
75 nffvmpt1 5873 . . . . . . . . . . . . . . . . . . . . 21
76 nffvmpt1 5873 . . . . . . . . . . . . . . . . . . . . . 22
77 nffvmpt1 5873 . . . . . . . . . . . . . . . . . . . . . 22
7876, 77nfop 4182 . . . . . . . . . . . . . . . . . . . . 21
7975, 78nfeq 2603 . . . . . . . . . . . . . . . . . . . 20
80 fveq2 5865 . . . . . . . . . . . . . . . . . . . . 21
81 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . 22
82 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . 22
8381, 82opeq12d 4174 . . . . . . . . . . . . . . . . . . . . 21
8480, 83eqeq12d 2466 . . . . . . . . . . . . . . . . . . . 20
8579, 84rspc 3144 . . . . . . . . . . . . . . . . . . 19
8673, 74, 85sylc 62 . . . . . . . . . . . . . . . . . 18
87 inss1 3652 . . . . . . . . . . . . . . . . . . . . 21
88 simpr 463 . . . . . . . . . . . . . . . . . . . . 21
8987, 88sseldi 3430 . . . . . . . . . . . . . . . . . . . 20
905ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . 22
91 ffun 5731 . . . . . . . . . . . . . . . . . . . . . 22
9290, 91syl 17 . . . . . . . . . . . . . . . . . . . . 21
9372adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23
94 fdm 5733 . . . . . . . . . . . . . . . . . . . . . . . 24
9590, 94syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
9693, 95sseqtr4d 3469 . . . . . . . . . . . . . . . . . . . . . 22
9796, 88sseldd 3433 . . . . . . . . . . . . . . . . . . . . 21
98 funfvima 6140 . . . . . . . . . . . . . . . . . . . . 21
9992, 97, 98syl2anc 667 . . . . . . . . . . . . . . . . . . . 20
10089, 99mpd 15 . . . . . . . . . . . . . . . . . . 19
101 inss2 3653 . . . . . . . . . . . . . . . . . . . . 21
102101, 88sseldi 3430 . . . . . . . . . . . . . . . . . . . 20
10313ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . 22
104 ffun 5731 . . . . . . . . . . . . . . . . . . . . . 22
105103, 104syl 17 . . . . . . . . . . . . . . . . . . . . 21
106 fdm 5733 . . . . . . . . . . . . . . . . . . . . . . . 24
107103, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
10893, 107sseqtr4d 3469 . . . . . . . . . . . . . . . . . . . . . 22
109108, 88sseldd 3433 . . . . . . . . . . . . . . . . . . . . 21
110 funfvima 6140 . . . . . . . . . . . . . . . . . . . . 21
111105, 109, 110syl2anc 667 . . . . . . . . . . . . . . . . . . . 20
112102, 111mpd 15 . . . . . . . . . . . . . . . . . . 19
113 opelxpi 4866 . . . . . . . . . . . . . . . . . . 19
114100, 112, 113syl2anc 667 . . . . . . . . . . . . . . . . . 18
11586, 114eqeltrd 2529 . . . . . . . . . . . . . . . . 17
116115ralrimiva 2802 . . . . . . . . . . . . . . . 16
117 ffun 5731 . . . . . . . . . . . . . . . . . . 19
11821, 117syl 17 . . . . . . . . . . . . . . . . . 18
119118adantr 467 . . . . . . . . . . . . . . . . 17
120 fdm 5733 . . . . . . . . . . . . . . . . . . . 20
12121, 120syl 17 . . . . . . . . . . . . . . . . . . 19
122121adantr 467 . . . . . . . . . . . . . . . . . 18
12372, 122sseqtr4d 3469 . . . . . . . . . . . . . . . . 17
124 funimass4 5916 . . . . . . . . . . . . . . . . 17
125119, 123, 124syl2anc 667 . . . . . . . . . . . . . . . 16
126116, 125mpbird 236 . . . . . . . . . . . . . . 15
12770, 126syldan 473 . . . . . . . . . . . . . 14
128127adantlr 721 . . . . . . . . . . . . 13
129 xpss12 4940 . . . . . . . . . . . . 13
130 sstr2 3439 . . . . . . . . . . . . 13
131128, 129, 130syl2im 39 . . . . . . . . . . . 12
13267, 131anim12d 566 . . . . . . . . . . 11
13364, 132syl5bi 221 . . . . . . . . . 10
134 topontop 19941 . . . . . . . . . . . . 13 TopOn
1351, 134syl 17 . . . . . . . . . . . 12
136 inopn 19929 . . . . . . . . . . . . 13
1371363expb 1209 . . . . . . . . . . . 12
138135, 137sylan 474 . . . . . . . . . . 11
139138adantlr 721 . . . . . . . . . 10
140133, 139jctild 546 . . . . . . . . 9
141140expimpd 608 . . . . . . . 8
142 eleq2 2518 . . . . . . . . . 10
143 imaeq2 5164 . . . . . . . . . . 11
144143sseq1d 3459 . . . . . . . . . 10
145142, 144anbi12d 717 . . . . . . . . 9
146145rspcev 3150 . . . . . . . 8
147141, 146syl6 34 . . . . . . 7
148147expd 438 . . . . . 6
149148rexlimdvv 2885 . . . . 5
15063, 149syld 45 . . . 4
151150ralrimivva 2809 . . 3
152 vex 3048 . . . . . 6
153 vex 3048 . . . . . 6
154152, 153xpex 6595 . . . . 5
155154rgen2w 2750 . . . 4
156 eqid 2451 . . . . 5
157 eleq2 2518 . . . . . 6
158 sseq2 3454 . . . . . . . 8
159158anbi2d 710 . . . . . . 7
160159rexbidv 2901 . . . . . 6
161157, 160imbi12d 322 . . . . 5
162156, 161ralrnmpt2 6411 . . . 4
163155, 162ax-mp 5 . . 3
164151, 163sylibr 216 . 2
165 topontop 19941 . . . . 5 TopOn
1662, 165syl 17 . . . 4
167 topontop 19941 . . . . 5 TopOn
16810, 167syl 17 . . . 4
169 eqid 2451 . . . . 5
170169txval 20579 . . . 4
171166, 168, 170syl2anc 667 . . 3
172 txtopon 20606 . . . 4 TopOn TopOn TopOn
1732, 10, 172syl2anc 667 . . 3 TopOn
1741, 171, 173, 22tgcnp 20269 . 2
17521, 164, 174mpbir2and 933 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1444   wcel 1887  wral 2737  wrex 2738  cvv 3045   cin 3403   wss 3404  cop 3974   cmpt 4461   cxp 4832   cdm 4834   crn 4835  cima 4837   wfun 5576  wf 5578  cfv 5582  (class class class)co 6290   cmpt2 6292  ctg 15336  ctop 19917  TopOnctopon 19918   ccnp 20241   ctx 20575 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-1st 6793  df-2nd 6794  df-map 7474  df-topgen 15342  df-top 19921  df-bases 19922  df-topon 19923  df-cnp 20244  df-tx 20577 This theorem is referenced by:  limccnp2  22847
 Copyright terms: Public domain W3C validator