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

Theorem ptcn 22211
 Description: If every projection of a function is continuous, then the function itself is continuous into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.)
Hypotheses
Ref Expression
ptcn.2 𝐾 = (∏t𝐹)
ptcn.3 (𝜑𝐽 ∈ (TopOn‘𝑋))
ptcn.4 (𝜑𝐼𝑉)
ptcn.5 (𝜑𝐹:𝐼⟶Top)
ptcn.6 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴) ∈ (𝐽 Cn (𝐹𝑘)))
Assertion
Ref Expression
ptcn (𝜑 → (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ (𝐽 Cn 𝐾))
Distinct variable groups:   𝑥,𝑘,𝐹   𝑘,𝐼,𝑥   𝑘,𝐽   𝜑,𝑘,𝑥   𝑘,𝑋,𝑥   𝑥,𝐾   𝑘,𝑉,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐽(𝑥)   𝐾(𝑘)

Proof of Theorem ptcn
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 ptcn.3 . . . . . . . . . 10 (𝜑𝐽 ∈ (TopOn‘𝑋))
21adantr 483 . . . . . . . . 9 ((𝜑𝑘𝐼) → 𝐽 ∈ (TopOn‘𝑋))
3 ptcn.5 . . . . . . . . . . 11 (𝜑𝐹:𝐼⟶Top)
43ffvelrnda 6827 . . . . . . . . . 10 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ Top)
5 toptopon2 21502 . . . . . . . . . 10 ((𝐹𝑘) ∈ Top ↔ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
64, 5sylib 220 . . . . . . . . 9 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
7 ptcn.6 . . . . . . . . 9 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴) ∈ (𝐽 Cn (𝐹𝑘)))
8 cnf2 21833 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)) ∧ (𝑥𝑋𝐴) ∈ (𝐽 Cn (𝐹𝑘))) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
92, 6, 7, 8syl3anc 1367 . . . . . . . 8 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
109fvmptelrn 6853 . . . . . . 7 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝐴 (𝐹𝑘))
1110an32s 650 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘𝐼) → 𝐴 (𝐹𝑘))
1211ralrimiva 3169 . . . . 5 ((𝜑𝑥𝑋) → ∀𝑘𝐼 𝐴 (𝐹𝑘))
13 ptcn.4 . . . . . . 7 (𝜑𝐼𝑉)
1413adantr 483 . . . . . 6 ((𝜑𝑥𝑋) → 𝐼𝑉)
15 mptelixpg 8477 . . . . . 6 (𝐼𝑉 → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐹𝑘) ↔ ∀𝑘𝐼 𝐴 (𝐹𝑘)))
1614, 15syl 17 . . . . 5 ((𝜑𝑥𝑋) → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐹𝑘) ↔ ∀𝑘𝐼 𝐴 (𝐹𝑘)))
1712, 16mpbird 259 . . . 4 ((𝜑𝑥𝑋) → (𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐹𝑘))
18 ptcn.2 . . . . . . 7 𝐾 = (∏t𝐹)
1918ptuni 22178 . . . . . 6 ((𝐼𝑉𝐹:𝐼⟶Top) → X𝑘𝐼 (𝐹𝑘) = 𝐾)
2013, 3, 19syl2anc 586 . . . . 5 (𝜑X𝑘𝐼 (𝐹𝑘) = 𝐾)
2120adantr 483 . . . 4 ((𝜑𝑥𝑋) → X𝑘𝐼 (𝐹𝑘) = 𝐾)
2217, 21eleqtrd 2913 . . 3 ((𝜑𝑥𝑋) → (𝑘𝐼𝐴) ∈ 𝐾)
2322fmpttd 6855 . 2 (𝜑 → (𝑥𝑋 ↦ (𝑘𝐼𝐴)):𝑋 𝐾)
241adantr 483 . . . 4 ((𝜑𝑧𝑋) → 𝐽 ∈ (TopOn‘𝑋))
2513adantr 483 . . . 4 ((𝜑𝑧𝑋) → 𝐼𝑉)
263adantr 483 . . . 4 ((𝜑𝑧𝑋) → 𝐹:𝐼⟶Top)
27 simpr 487 . . . 4 ((𝜑𝑧𝑋) → 𝑧𝑋)
287adantlr 713 . . . . 5 (((𝜑𝑧𝑋) ∧ 𝑘𝐼) → (𝑥𝑋𝐴) ∈ (𝐽 Cn (𝐹𝑘)))
29 simplr 767 . . . . . 6 (((𝜑𝑧𝑋) ∧ 𝑘𝐼) → 𝑧𝑋)
30 toponuni 21498 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
311, 30syl 17 . . . . . . 7 (𝜑𝑋 = 𝐽)
3231ad2antrr 724 . . . . . 6 (((𝜑𝑧𝑋) ∧ 𝑘𝐼) → 𝑋 = 𝐽)
3329, 32eleqtrd 2913 . . . . 5 (((𝜑𝑧𝑋) ∧ 𝑘𝐼) → 𝑧 𝐽)
34 eqid 2820 . . . . . 6 𝐽 = 𝐽
3534cncnpi 21862 . . . . 5 (((𝑥𝑋𝐴) ∈ (𝐽 Cn (𝐹𝑘)) ∧ 𝑧 𝐽) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝑧))
3628, 33, 35syl2anc 586 . . . 4 (((𝜑𝑧𝑋) ∧ 𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝑧))
3718, 24, 25, 26, 27, 36ptcnp 22206 . . 3 ((𝜑𝑧𝑋) → (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝑧))
3837ralrimiva 3169 . 2 (𝜑 → ∀𝑧𝑋 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝑧))
39 pttop 22166 . . . . . 6 ((𝐼𝑉𝐹:𝐼⟶Top) → (∏t𝐹) ∈ Top)
4013, 3, 39syl2anc 586 . . . . 5 (𝜑 → (∏t𝐹) ∈ Top)
4118, 40eqeltrid 2915 . . . 4 (𝜑𝐾 ∈ Top)
42 toptopon2 21502 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
4341, 42sylib 220 . . 3 (𝜑𝐾 ∈ (TopOn‘ 𝐾))
44 cncnp 21864 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘ 𝐾)) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ (𝐽 Cn 𝐾) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)):𝑋 𝐾 ∧ ∀𝑧𝑋 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝑧))))
451, 43, 44syl2anc 586 . 2 (𝜑 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ (𝐽 Cn 𝐾) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)):𝑋 𝐾 ∧ ∀𝑧𝑋 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝑧))))
4623, 38, 45mpbir2and 711 1 (𝜑 → (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ (𝐽 Cn 𝐾))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3125  ∪ cuni 4814   ↦ cmpt 5122  ⟶wf 6327  ‘cfv 6331  (class class class)co 7133  Xcixp 8439  ∏tcpt 16691  Topctop 21477  TopOnctopon 21494   Cn ccn 21808   CnP ccnp 21809 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-iin 4898  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-1st 7667  df-2nd 7668  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-oadd 8084  df-er 8267  df-map 8386  df-ixp 8440  df-en 8488  df-dom 8489  df-fin 8491  df-fi 8853  df-topgen 16696  df-pt 16697  df-top 21478  df-topon 21495  df-bases 21530  df-cn 21811  df-cnp 21812 This theorem is referenced by:  pt1hmeo  22390  ptunhmeo  22392  symgtgp  22690  prdstmdd  22708  prdstgpd  22709  ptpconn  32488  broucube  34967
 Copyright terms: Public domain W3C validator