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

Theorem txtop 23518
Description: The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
txtop ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)

Proof of Theorem txtop
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2737 . . 3 ran (𝑢𝑅, 𝑣𝑆 ↦ (𝑢 × 𝑣)) = ran (𝑢𝑅, 𝑣𝑆 ↦ (𝑢 × 𝑣))
21txval 23513 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) = (topGen‘ran (𝑢𝑅, 𝑣𝑆 ↦ (𝑢 × 𝑣))))
3 topbas 22921 . . . 4 (𝑅 ∈ Top → 𝑅 ∈ TopBases)
4 topbas 22921 . . . 4 (𝑆 ∈ Top → 𝑆 ∈ TopBases)
51txbas 23516 . . . 4 ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ran (𝑢𝑅, 𝑣𝑆 ↦ (𝑢 × 𝑣)) ∈ TopBases)
63, 4, 5syl2an 597 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ran (𝑢𝑅, 𝑣𝑆 ↦ (𝑢 × 𝑣)) ∈ TopBases)
7 tgcl 22918 . . 3 (ran (𝑢𝑅, 𝑣𝑆 ↦ (𝑢 × 𝑣)) ∈ TopBases → (topGen‘ran (𝑢𝑅, 𝑣𝑆 ↦ (𝑢 × 𝑣))) ∈ Top)
86, 7syl 17 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (topGen‘ran (𝑢𝑅, 𝑣𝑆 ↦ (𝑢 × 𝑣))) ∈ Top)
92, 8eqeltrd 2837 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2114   × cxp 5623  ran crn 5626  cfv 6493  (class class class)co 7361  cmpo 7363  topGenctg 17362  Topctop 22842  TopBasesctb 22894   ×t ctx 23509
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7683
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-topgen 17368  df-top 22843  df-bases 22895  df-tx 23511
This theorem is referenced by:  txtopi  23539  txtopon  23540  txcld  23552  neitx  23556  txlly  23585  txnlly  23586  txcmplem1  23590  txcmp  23592  hausdiag  23594  txhaus  23596  tx1stc  23599  txkgen  23601  xkococn  23609  xkoinjcn  23636  txconn  23638  imasnopn  23639  imasncls  23641  utop2nei  24199  utop3cls  24200  qtophaus  34006  txpconn  35439
  Copyright terms: Public domain W3C validator