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

Theorem ptcn 21478
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 . . . . . . . . . . 11 (𝜑𝐽 ∈ (TopOn‘𝑋))
21adantr 480 . . . . . . . . . 10 ((𝜑𝑘𝐼) → 𝐽 ∈ (TopOn‘𝑋))
3 ptcn.5 . . . . . . . . . . . 12 (𝜑𝐹:𝐼⟶Top)
43ffvelrnda 6399 . . . . . . . . . . 11 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ Top)
5 eqid 2651 . . . . . . . . . . . 12 (𝐹𝑘) = (𝐹𝑘)
65toptopon 20770 . . . . . . . . . . 11 ((𝐹𝑘) ∈ Top ↔ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
74, 6sylib 208 . . . . . . . . . 10 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
8 ptcn.6 . . . . . . . . . 10 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴) ∈ (𝐽 Cn (𝐹𝑘)))
9 cnf2 21101 . . . . . . . . . 10 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)) ∧ (𝑥𝑋𝐴) ∈ (𝐽 Cn (𝐹𝑘))) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
102, 7, 8, 9syl3anc 1366 . . . . . . . . 9 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
11 eqid 2651 . . . . . . . . . 10 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
1211fmpt 6421 . . . . . . . . 9 (∀𝑥𝑋 𝐴 (𝐹𝑘) ↔ (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
1310, 12sylibr 224 . . . . . . . 8 ((𝜑𝑘𝐼) → ∀𝑥𝑋 𝐴 (𝐹𝑘))
1413r19.21bi 2961 . . . . . . 7 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝐴 (𝐹𝑘))
1514an32s 863 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘𝐼) → 𝐴 (𝐹𝑘))
1615ralrimiva 2995 . . . . 5 ((𝜑𝑥𝑋) → ∀𝑘𝐼 𝐴 (𝐹𝑘))
17 ptcn.4 . . . . . . 7 (𝜑𝐼𝑉)
1817adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → 𝐼𝑉)
19 mptelixpg 7987 . . . . . 6 (𝐼𝑉 → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐹𝑘) ↔ ∀𝑘𝐼 𝐴 (𝐹𝑘)))
2018, 19syl 17 . . . . 5 ((𝜑𝑥𝑋) → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐹𝑘) ↔ ∀𝑘𝐼 𝐴 (𝐹𝑘)))
2116, 20mpbird 247 . . . 4 ((𝜑𝑥𝑋) → (𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐹𝑘))
22 ptcn.2 . . . . . . 7 𝐾 = (∏t𝐹)
2322ptuni 21445 . . . . . 6 ((𝐼𝑉𝐹:𝐼⟶Top) → X𝑘𝐼 (𝐹𝑘) = 𝐾)
2417, 3, 23syl2anc 694 . . . . 5 (𝜑X𝑘𝐼 (𝐹𝑘) = 𝐾)
2524adantr 480 . . . 4 ((𝜑𝑥𝑋) → X𝑘𝐼 (𝐹𝑘) = 𝐾)
2621, 25eleqtrd 2732 . . 3 ((𝜑𝑥𝑋) → (𝑘𝐼𝐴) ∈ 𝐾)
27 eqid 2651 . . 3 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = (𝑥𝑋 ↦ (𝑘𝐼𝐴))
2826, 27fmptd 6425 . 2 (𝜑 → (𝑥𝑋 ↦ (𝑘𝐼𝐴)):𝑋 𝐾)
291adantr 480 . . . 4 ((𝜑𝑧𝑋) → 𝐽 ∈ (TopOn‘𝑋))
3017adantr 480 . . . 4 ((𝜑𝑧𝑋) → 𝐼𝑉)
313adantr 480 . . . 4 ((𝜑𝑧𝑋) → 𝐹:𝐼⟶Top)
32 simpr 476 . . . 4 ((𝜑𝑧𝑋) → 𝑧𝑋)
338adantlr 751 . . . . 5 (((𝜑𝑧𝑋) ∧ 𝑘𝐼) → (𝑥𝑋𝐴) ∈ (𝐽 Cn (𝐹𝑘)))
34 simplr 807 . . . . . 6 (((𝜑𝑧𝑋) ∧ 𝑘𝐼) → 𝑧𝑋)
35 toponuni 20767 . . . . . . . 8 (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = 𝐽)
361, 35syl 17 . . . . . . 7 (𝜑𝑋 = 𝐽)
3736ad2antrr 762 . . . . . 6 (((𝜑𝑧𝑋) ∧ 𝑘𝐼) → 𝑋 = 𝐽)
3834, 37eleqtrd 2732 . . . . 5 (((𝜑𝑧𝑋) ∧ 𝑘𝐼) → 𝑧 𝐽)
39 eqid 2651 . . . . . 6 𝐽 = 𝐽
4039cncnpi 21130 . . . . 5 (((𝑥𝑋𝐴) ∈ (𝐽 Cn (𝐹𝑘)) ∧ 𝑧 𝐽) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝑧))
4133, 38, 40syl2anc 694 . . . 4 (((𝜑𝑧𝑋) ∧ 𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝑧))
4222, 29, 30, 31, 32, 41ptcnp 21473 . . 3 ((𝜑𝑧𝑋) → (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝑧))
4342ralrimiva 2995 . 2 (𝜑 → ∀𝑧𝑋 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝑧))
44 pttop 21433 . . . . . 6 ((𝐼𝑉𝐹:𝐼⟶Top) → (∏t𝐹) ∈ Top)
4517, 3, 44syl2anc 694 . . . . 5 (𝜑 → (∏t𝐹) ∈ Top)
4622, 45syl5eqel 2734 . . . 4 (𝜑𝐾 ∈ Top)
47 eqid 2651 . . . . 5 𝐾 = 𝐾
4847toptopon 20770 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
4946, 48sylib 208 . . 3 (𝜑𝐾 ∈ (TopOn‘ 𝐾))
50 cncnp 21132 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘ 𝐾)) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ (𝐽 Cn 𝐾) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)):𝑋 𝐾 ∧ ∀𝑧𝑋 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝑧))))
511, 49, 50syl2anc 694 . 2 (𝜑 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ (𝐽 Cn 𝐾) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)):𝑋 𝐾 ∧ ∀𝑧𝑋 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝑧))))
5228, 43, 51mpbir2and 977 1 (𝜑 → (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ (𝐽 Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941   cuni 4468  cmpt 4762  wf 5922  cfv 5926  (class class class)co 6690  Xcixp 7950  tcpt 16146  Topctop 20746  TopOnctopon 20763   Cn ccn 21076   CnP ccnp 21077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-fin 8001  df-fi 8358  df-topgen 16151  df-pt 16152  df-top 20747  df-topon 20764  df-bases 20798  df-cn 21079  df-cnp 21080
This theorem is referenced by:  pt1hmeo  21657  ptunhmeo  21659  symgtgp  21952  prdstmdd  21974  prdstgpd  21975  ptpconn  31341  broucube  33573
  Copyright terms: Public domain W3C validator