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

Theorem txcnp 17657
 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 17319 . . . . . . 7 TopOn TopOn
51, 2, 3, 4syl3anc 1185 . . . . . 6
6 eqid 2438 . . . . . . 7
76fmpt 5893 . . . . . 6
85, 7sylibr 205 . . . . 5
98r19.21bi 2806 . . . 4
10 txcnp.6 . . . . . . 7 TopOn
11 txcnp.9 . . . . . . 7
12 cnpf2 17319 . . . . . . 7 TopOn TopOn
131, 10, 11, 12syl3anc 1185 . . . . . 6
14 eqid 2438 . . . . . . 7
1514fmpt 5893 . . . . . 6
1613, 15sylibr 205 . . . . 5
1716r19.21bi 2806 . . . 4
18 opelxpi 4913 . . . 4
199, 17, 18syl2anc 644 . . 3
20 eqid 2438 . . 3
2119, 20fmptd 5896 . 2
22 txcnp.7 . . . . . . . . 9
23 simpr 449 . . . . . . . . . . . 12
24 opex 4430 . . . . . . . . . . . 12
2520fvmpt2 5815 . . . . . . . . . . . 12
2623, 24, 25sylancl 645 . . . . . . . . . . 11
276fvmpt2 5815 . . . . . . . . . . . . 13
2823, 9, 27syl2anc 644 . . . . . . . . . . . 12
2914fvmpt2 5815 . . . . . . . . . . . . 13
3023, 17, 29syl2anc 644 . . . . . . . . . . . 12
3128, 30opeq12d 3994 . . . . . . . . . . 11
3226, 31eqtr4d 2473 . . . . . . . . . 10
3332ralrimiva 2791 . . . . . . . . 9
34 nffvmpt1 5739 . . . . . . . . . . 11
35 nffvmpt1 5739 . . . . . . . . . . . 12
36 nffvmpt1 5739 . . . . . . . . . . . 12
3735, 36nfop 4002 . . . . . . . . . . 11
3834, 37nfeq 2581 . . . . . . . . . 10
39 fveq2 5731 . . . . . . . . . . 11
40 fveq2 5731 . . . . . . . . . . . 12
41 fveq2 5731 . . . . . . . . . . . 12
4240, 41opeq12d 3994 . . . . . . . . . . 11
4339, 42eqeq12d 2452 . . . . . . . . . 10
4438, 43rspc 3048 . . . . . . . . 9
4522, 33, 44sylc 59 . . . . . . . 8
4645eleq1d 2504 . . . . . . 7
4746adantr 453 . . . . . 6
483ad2antrr 708 . . . . . . . . . 10
49 simplrl 738 . . . . . . . . . 10
50 simprl 734 . . . . . . . . . 10
51 cnpimaex 17325 . . . . . . . . . 10
5248, 49, 50, 51syl3anc 1185 . . . . . . . . 9
5311ad2antrr 708 . . . . . . . . . 10
54 simplrr 739 . . . . . . . . . 10
55 simprr 735 . . . . . . . . . 10
56 cnpimaex 17325 . . . . . . . . . 10
5753, 54, 55, 56syl3anc 1185 . . . . . . . . 9
5852, 57jca 520 . . . . . . . 8
5958ex 425 . . . . . . 7
60 opelxp 4911 . . . . . . 7
61 reeanv 2877 . . . . . . 7
6259, 60, 613imtr4g 263 . . . . . 6
6347, 62sylbid 208 . . . . 5
64 an4 799 . . . . . . . . . . 11
65 elin 3532 . . . . . . . . . . . . . 14
6665biimpri 199 . . . . . . . . . . . . 13
6766a1i 11 . . . . . . . . . . . 12
68 simpl 445 . . . . . . . . . . . . . . . 16
69 toponss 16999 . . . . . . . . . . . . . . . 16 TopOn
701, 68, 69syl2an 465 . . . . . . . . . . . . . . 15
71 ssinss1 3571 . . . . . . . . . . . . . . . . . . . . 21
7271adantl 454 . . . . . . . . . . . . . . . . . . . 20
7372sselda 3350 . . . . . . . . . . . . . . . . . . 19
7433ad2antrr 708 . . . . . . . . . . . . . . . . . . 19
75 nffvmpt1 5739 . . . . . . . . . . . . . . . . . . . . 21
76 nffvmpt1 5739 . . . . . . . . . . . . . . . . . . . . . 22
77 nffvmpt1 5739 . . . . . . . . . . . . . . . . . . . . . 22
7876, 77nfop 4002 . . . . . . . . . . . . . . . . . . . . 21
7975, 78nfeq 2581 . . . . . . . . . . . . . . . . . . . 20
80 fveq2 5731 . . . . . . . . . . . . . . . . . . . . 21
81 fveq2 5731 . . . . . . . . . . . . . . . . . . . . . 22
82 fveq2 5731 . . . . . . . . . . . . . . . . . . . . . 22
8381, 82opeq12d 3994 . . . . . . . . . . . . . . . . . . . . 21
8480, 83eqeq12d 2452 . . . . . . . . . . . . . . . . . . . 20
8579, 84rspc 3048 . . . . . . . . . . . . . . . . . . 19
8673, 74, 85sylc 59 . . . . . . . . . . . . . . . . . 18
87 inss1 3563 . . . . . . . . . . . . . . . . . . . . 21
88 simpr 449 . . . . . . . . . . . . . . . . . . . . 21
8987, 88sseldi 3348 . . . . . . . . . . . . . . . . . . . 20
905ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22
91 ffun 5596 . . . . . . . . . . . . . . . . . . . . . 22
9290, 91syl 16 . . . . . . . . . . . . . . . . . . . . 21
9372adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23
94 fdm 5598 . . . . . . . . . . . . . . . . . . . . . . . 24
9590, 94syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
9693, 95sseqtr4d 3387 . . . . . . . . . . . . . . . . . . . . . 22
9796, 88sseldd 3351 . . . . . . . . . . . . . . . . . . . . 21
98 funfvima 5976 . . . . . . . . . . . . . . . . . . . . 21
9992, 97, 98syl2anc 644 . . . . . . . . . . . . . . . . . . . 20
10089, 99mpd 15 . . . . . . . . . . . . . . . . . . 19
101 inss2 3564 . . . . . . . . . . . . . . . . . . . . 21
102101, 88sseldi 3348 . . . . . . . . . . . . . . . . . . . 20
10313ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22
104 ffun 5596 . . . . . . . . . . . . . . . . . . . . . 22
105103, 104syl 16 . . . . . . . . . . . . . . . . . . . . 21
106 fdm 5598 . . . . . . . . . . . . . . . . . . . . . . . 24
107103, 106syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
10893, 107sseqtr4d 3387 . . . . . . . . . . . . . . . . . . . . . 22
109108, 88sseldd 3351 . . . . . . . . . . . . . . . . . . . . 21
110 funfvima 5976 . . . . . . . . . . . . . . . . . . . . 21
111105, 109, 110syl2anc 644 . . . . . . . . . . . . . . . . . . . 20
112102, 111mpd 15 . . . . . . . . . . . . . . . . . . 19
113 opelxpi 4913 . . . . . . . . . . . . . . . . . . 19
114100, 112, 113syl2anc 644 . . . . . . . . . . . . . . . . . 18
11586, 114eqeltrd 2512 . . . . . . . . . . . . . . . . 17
116115ralrimiva 2791 . . . . . . . . . . . . . . . 16
117 ffun 5596 . . . . . . . . . . . . . . . . . . 19
11821, 117syl 16 . . . . . . . . . . . . . . . . . 18
119118adantr 453 . . . . . . . . . . . . . . . . 17
120 fdm 5598 . . . . . . . . . . . . . . . . . . . 20
12121, 120syl 16 . . . . . . . . . . . . . . . . . . 19
122121adantr 453 . . . . . . . . . . . . . . . . . 18
12372, 122sseqtr4d 3387 . . . . . . . . . . . . . . . . 17
124 funimass4 5780 . . . . . . . . . . . . . . . . 17
125119, 123, 124syl2anc 644 . . . . . . . . . . . . . . . 16
126116, 125mpbird 225 . . . . . . . . . . . . . . 15
12770, 126syldan 458 . . . . . . . . . . . . . 14
128127adantlr 697 . . . . . . . . . . . . 13
129 xpss12 4984 . . . . . . . . . . . . 13
130 sstr2 3357 . . . . . . . . . . . . 13
131128, 129, 130syl2im 37 . . . . . . . . . . . 12
13267, 131anim12d 548 . . . . . . . . . . 11
13364, 132syl5bi 210 . . . . . . . . . 10
134 topontop 16996 . . . . . . . . . . . . 13 TopOn
1351, 134syl 16 . . . . . . . . . . . 12
136 inopn 16977 . . . . . . . . . . . . 13
1371363expb 1155 . . . . . . . . . . . 12
138135, 137sylan 459 . . . . . . . . . . 11
139138adantlr 697 . . . . . . . . . 10
140133, 139jctild 529 . . . . . . . . 9
141140expimpd 588 . . . . . . . 8
142 eleq2 2499 . . . . . . . . . 10
143 imaeq2 5202 . . . . . . . . . . 11
144143sseq1d 3377 . . . . . . . . . 10
145142, 144anbi12d 693 . . . . . . . . 9
146145rspcev 3054 . . . . . . . 8
147141, 146syl6 32 . . . . . . 7
148147exp3a 427 . . . . . 6
149148rexlimdvv 2838 . . . . 5
15063, 149syld 43 . . . 4
151150ralrimivva 2800 . . 3
152 vex 2961 . . . . . 6
153 vex 2961 . . . . . 6
154152, 153xpex 4993 . . . . 5
155154rgen2w 2776 . . . 4
156 eqid 2438 . . . . 5
157 eleq2 2499 . . . . . 6
158 sseq2 3372 . . . . . . . 8
159158anbi2d 686 . . . . . . 7
160159rexbidv 2728 . . . . . 6
161157, 160imbi12d 313 . . . . 5
162156, 161ralrnmpt2 6187 . . . 4
163155, 162ax-mp 5 . . 3
164151, 163sylibr 205 . 2
165 topontop 16996 . . . . 5 TopOn
1662, 165syl 16 . . . 4
167 topontop 16996 . . . . 5 TopOn
16810, 167syl 16 . . . 4
169 eqid 2438 . . . . 5
170169txval 17601 . . . 4
171166, 168, 170syl2anc 644 . . 3
172 txtopon 17628 . . . 4 TopOn TopOn TopOn
1732, 10, 172syl2anc 644 . . 3 TopOn
1741, 171, 173, 22tgcnp 17322 . 2
17521, 164, 174mpbir2and 890 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   wceq 1653   wcel 1726  wral 2707  wrex 2708  cvv 2958   cin 3321   wss 3322  cop 3819   cmpt 4269   cxp 4879   cdm 4881   crn 4882  cima 4884   wfun 5451  wf 5453  cfv 5457  (class class class)co 6084   cmpt2 6086  ctg 13670  ctop 16963  TopOnctopon 16964   ccnp 17294   ctx 17597 This theorem is referenced by:  limccnp2  19784 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-iun 4097  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-fv 5465  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-map 7023  df-topgen 13672  df-top 16968  df-bases 16970  df-topon 16971  df-cnp 17297  df-tx 17599
 Copyright terms: Public domain W3C validator