Theorem txtopon 21604

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.

Step	Hyp	Ref	Expression
1		topontop 20927	. . 3 ⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top)
2		topontop 20927	. . 3 ⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑆 ∈ Top)
3		txtop 21582	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
4	1, 2, 3	syl2an 585	. 2 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ Top)
5		eqid 2806	. . . . 5 ⊢ ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣)) = ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣))
6		eqid 2806	. . . . 5 ⊢ ∪ 𝑅 = ∪ 𝑅
7		eqid 2806	. . . . 5 ⊢ ∪ 𝑆 = ∪ 𝑆
8	5, 6, 7	txuni2 21578	. . . 4 ⊢ (∪ 𝑅 × ∪ 𝑆) = ∪ ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣))
9		toponuni 20928	. . . . 5 ⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑅)
10		toponuni 20928	. . . . 5 ⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝑆)
11		xpeq12 5335	. . . . 5 ⊢ ((𝑋 = ∪ 𝑅 ∧ 𝑌 = ∪ 𝑆) → (𝑋 × 𝑌) = (∪ 𝑅 × ∪ 𝑆))
12	9, 10, 11	syl2an 585	. . . 4 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑋 × 𝑌) = (∪ 𝑅 × ∪ 𝑆))
13	5	txbasex 21579	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣)) ∈ V)
14		unitg 20981	. . . . 5 ⊢ (ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣)) ∈ V → ∪ (topGen‘ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣))) = ∪ ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣)))
15	13, 14	syl 17	. . . 4 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ∪ (topGen‘ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣))) = ∪ ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣)))
16	8, 12, 15	3eqtr4a 2866	. . 3 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑋 × 𝑌) = ∪ (topGen‘ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣))))
17	5	txval 21577	. . . 4 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) = (topGen‘ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣))))
18	17	unieqd 4640	. . 3 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → ∪ (𝑅 ×t 𝑆) = ∪ (topGen‘ran (𝑢 ∈ 𝑅, 𝑣 ∈ 𝑆 ↦ (𝑢 × 𝑣))))
19	16, 18	eqtr4d 2843	. 2 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆))
20		istopon 20926	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)))
21	4, 19, 20	sylanbrc 574	1 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)))

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1637   ∈ wcel 2156  Vcvv 3391  ∪ cuni 4630   × cxp 5309  ran crn 5312  ‘cfv 6097  (class class class)co 6870   ↦ cmpt2 6872  topGenctg 16299  Topctop 20907  TopOnctopon 20924   ×_t ctx 21573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-fv 6105  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-1st 7394  df-2nd 7395  df-topgen 16305  df-top 20908  df-topon 20925  df-bases 20960  df-tx 21575

This theorem is referenced by:  txuni  21605  txcls  21617  tx1cn  21622  tx2cn  21623  txcnp  21633  txcnmpt  21637  txindis  21647  txdis1cn  21648  txlm  21661  lmcn2  21662  xkococn  21673  cnmpt12  21680  cnmpt2c  21683  cnmpt21  21684  cnmpt2t  21686  cnmpt22  21687  cnmpt22f  21688  cnmpt2res  21690  cnmptcom  21691  cnmpt2k  21701  ptunhmeo  21821  xpstopnlem1  21822  xkocnv  21827  xkohmeo  21828  txflf  22019  flfcnp2  22020  cnmpt2plusg  22101  tmdcn2  22102  indistgp  22113  clssubg  22121  qustgplem  22133  prdstmdd  22136  tsmsadd  22159  cnmpt2vsca  22207  txmetcn  22562  cnmpt2ds  22855  fsum2cn  22883  cnmpt2pc  22936  htpyco2  22987  phtpyco2  22998  cnmpt2ip  23255  limccnp2  23866  dvcnp2  23893  dvaddbr  23911  dvmulbr  23912  dvcobr  23919  lhop1lem  23986  taylthlem2  24338  cxpcn3  24699  tpr2tp  30271  txsconnlem  31540  txsconn  31541  cvmlift2lem11  31613  cvmlift2lem12  31614