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

Theorem cnmpt1st 22565
Description: The projection onto the first coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
cnmpt21.j (𝜑𝐽 ∈ (TopOn‘𝑋))
cnmpt21.k (𝜑𝐾 ∈ (TopOn‘𝑌))
Assertion
Ref Expression
cnmpt1st (𝜑 → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
Distinct variable groups:   𝑥,𝑦,𝜑   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦
Allowed substitution hints:   𝐽(𝑥,𝑦)   𝐾(𝑥,𝑦)

Proof of Theorem cnmpt1st
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 fo1st 7781 . . . . . 6 1st :V–onto→V
2 fofn 6635 . . . . . 6 (1st :V–onto→V → 1st Fn V)
31, 2ax-mp 5 . . . . 5 1st Fn V
4 ssv 3925 . . . . 5 (𝑋 × 𝑌) ⊆ V
5 fnssres 6500 . . . . 5 ((1st Fn V ∧ (𝑋 × 𝑌) ⊆ V) → (1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
63, 4, 5mp2an 692 . . . 4 (1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
7 dffn5 6771 . . . 4 ((1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ↔ (1st ↾ (𝑋 × 𝑌)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ↾ (𝑋 × 𝑌))‘𝑧)))
86, 7mpbi 233 . . 3 (1st ↾ (𝑋 × 𝑌)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ↾ (𝑋 × 𝑌))‘𝑧))
9 fvres 6736 . . . 4 (𝑧 ∈ (𝑋 × 𝑌) → ((1st ↾ (𝑋 × 𝑌))‘𝑧) = (1st𝑧))
109mpteq2ia 5146 . . 3 (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ↾ (𝑋 × 𝑌))‘𝑧)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧))
11 vex 3412 . . . . 5 𝑥 ∈ V
12 vex 3412 . . . . 5 𝑦 ∈ V
1311, 12op1std 7771 . . . 4 (𝑧 = ⟨𝑥, 𝑦⟩ → (1st𝑧) = 𝑥)
1413mpompt 7324 . . 3 (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st𝑧)) = (𝑥𝑋, 𝑦𝑌𝑥)
158, 10, 143eqtri 2769 . 2 (1st ↾ (𝑋 × 𝑌)) = (𝑥𝑋, 𝑦𝑌𝑥)
16 cnmpt21.j . . 3 (𝜑𝐽 ∈ (TopOn‘𝑋))
17 cnmpt21.k . . 3 (𝜑𝐾 ∈ (TopOn‘𝑌))
18 tx1cn 22506 . . 3 ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
1916, 17, 18syl2anc 587 . 2 (𝜑 → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
2015, 19eqeltrrid 2843 1 (𝜑 → (𝑥𝑋, 𝑦𝑌𝑥) ∈ ((𝐽 ×t 𝐾) Cn 𝐽))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wcel 2110  Vcvv 3408  wss 3866  cmpt 5135   × cxp 5549  cres 5553   Fn wfn 6375  ontowfo 6378  cfv 6380  (class class class)co 7213  cmpo 7215  1st c1st 7759  TopOnctopon 21807   Cn ccn 22121   ×t ctx 22457
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-fo 6386  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-1st 7761  df-2nd 7762  df-map 8510  df-topgen 16948  df-top 21791  df-topon 21808  df-bases 21843  df-cn 22124  df-tx 22459
This theorem is referenced by:  cnmptcom  22575  xkofvcn  22581  cnmptk2  22583  txhmeo  22700  txswaphmeo  22702  ptunhmeo  22705  xkohmeo  22712  tgpsubcn  22987  istgp2  22988  oppgtmd  22994  prdstmdd  23021  dvrcn  23081  divcn  23765  cnrehmeo  23850  htpycom  23873  htpyid  23874  htpyco1  23875  htpycc  23877  reparphti  23894  pcocn  23914  pcohtpylem  23916  pcopt  23919  pcopt2  23920  pcoass  23921  pcorevlem  23923  cxpcn  25631  vmcn  28780  dipcn  28801  mndpluscn  31590  cvxsconn  32918  cvmlift2lem12  32989
  Copyright terms: Public domain W3C validator