MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txtopon Structured version   Visualization version   GIF version
Theorem txtopon 23315
Description: The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 22-Aug-2015.) (Revised by Mario Carneiro, 2-Sep-2015.)
Assertion
Ref Expression
txtopon ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝑅 Γ—t 𝑆) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
Proof of Theorem txtopon
Dummy variables 𝑣 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 topontop 22635 . . 3 (𝑅 ∈ (TopOnβ€˜π‘‹) β†’ 𝑅 ∈ Top)
2 topontop 22635 . . 3 (𝑆 ∈ (TopOnβ€˜π‘Œ) β†’ 𝑆 ∈ Top)
3 txtop 23293 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
41, 2, 3syl2an 596 . 2 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝑅 Γ—t 𝑆) ∈ Top)
5 eqid 2732 . . . . 5 ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣)) = ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣))
6 eqid 2732 . . . . 5 βˆͺ 𝑅 = βˆͺ 𝑅
7 eqid 2732 . . . . 5 βˆͺ 𝑆 = βˆͺ 𝑆
85, 6, 7txuni2 23289 . . . 4 (βˆͺ 𝑅 Γ— βˆͺ 𝑆) = βˆͺ ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣))
9 toponuni 22636 . . . . 5 (𝑅 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝑅)
10 toponuni 22636 . . . . 5 (𝑆 ∈ (TopOnβ€˜π‘Œ) β†’ π‘Œ = βˆͺ 𝑆)
11 xpeq12 5701 . . . . 5 ((𝑋 = βˆͺ 𝑅 ∧ π‘Œ = βˆͺ 𝑆) β†’ (𝑋 Γ— π‘Œ) = (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
129, 10, 11syl2an 596 . . . 4 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝑋 Γ— π‘Œ) = (βˆͺ 𝑅 Γ— βˆͺ 𝑆))
135txbasex 23290 . . . . 5 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣)) ∈ V)
14 unitg 22690 . . . . 5 (ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣)) ∈ V β†’ βˆͺ (topGenβ€˜ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣))) = βˆͺ ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣)))
1513, 14syl 17 . . . 4 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ βˆͺ (topGenβ€˜ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣))) = βˆͺ ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣)))
168, 12, 153eqtr4a 2798 . . 3 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝑋 Γ— π‘Œ) = βˆͺ (topGenβ€˜ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣))))
175txval 23288 . . . 4 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝑅 Γ—t 𝑆) = (topGenβ€˜ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣))))
1817unieqd 4922 . . 3 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ βˆͺ (𝑅 Γ—t 𝑆) = βˆͺ (topGenβ€˜ran (𝑒 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑒 Γ— 𝑣))))
1916, 18eqtr4d 2775 . 2 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝑋 Γ— π‘Œ) = βˆͺ (𝑅 Γ—t 𝑆))
20 istopon 22634 . 2 ((𝑅 Γ—t 𝑆) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)) ↔ ((𝑅 Γ—t 𝑆) ∈ Top ∧ (𝑋 Γ— π‘Œ) = βˆͺ (𝑅 Γ—t 𝑆)))
214, 19, 20sylanbrc 583 1 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝑅 Γ—t 𝑆) ∈ (TopOnβ€˜(𝑋 Γ— π‘Œ)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3474  βˆͺ cuni 4908   Γ— cxp 5674  ran crn 5677  β€˜cfv 6543  (class class class)co 7411   ∈ cmpo 7413  topGenctg 17387  Topctop 22615  TopOnctopon 22632   Γ—t ctx 23284
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-topgen 17393  df-top 22616  df-topon 22633  df-bases 22669  df-tx 23286
This theorem is referenced by:  txuni  23316  txcls  23328  tx1cn  23333  tx2cn  23334  txcnp  23344  txcnmpt  23348  txindis  23358  txdis1cn  23359  txlm  23372  lmcn2  23373  xkococn  23384  cnmpt12  23391  cnmpt2c  23394  cnmpt21  23395  cnmpt2t  23397  cnmpt22  23398  cnmpt22f  23399  cnmpt2res  23401  cnmptcom  23402  cnmpt2k  23412  ptunhmeo  23532  xpstopnlem1  23533  xkocnv  23538  xkohmeo  23539  txflf  23730  flfcnp2  23731  cnmpt2plusg  23812  tmdcn2  23813  indistgp  23824  clssubg  23833  qustgplem  23845  prdstmdd  23848  tsmsadd  23871  cnmpt2vsca  23919  txmetcn  24277  cnmpt2ds  24579  fsum2cn  24609  cnmpopc  24668  htpyco2  24719  phtpyco2  24730  cnmpt2ip  24989  limccnp2  25633  dvcnp2  25661  dvaddbr  25679  dvmulbr  25680  dvcobr  25687  lhop1lem  25754  taylthlem2  26110  cxpcn3  26480  tpr2tp  33170  txsconnlem  34517  txsconn  34518  cvmlift2lem11  34590  cvmlift2lem12  34591  gg-dvcnp2  35460  gg-dvmulbr  35461  gg-dvcobr  35462
  Copyright terms: Public domain W3C validator