MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  txcn Structured version   Visualization version   GIF version
Theorem txcn 23121
Description: A map into the product of two topological spaces is continuous iff both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
txcn.1 𝑋 = βˆͺ 𝑅
txcn.2 π‘Œ = βˆͺ 𝑆
txcn.3 𝑍 = (𝑋 Γ— π‘Œ)
txcn.4 π‘Š = βˆͺ π‘ˆ
txcn.5 𝑃 = (1st β†Ύ 𝑍)
txcn.6 𝑄 = (2nd β†Ύ 𝑍)
Assertion
Ref Expression
txcn ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) β†’ (𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ↔ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))))
Proof of Theorem txcn
Dummy variable β„Ž is distinct from all other variables.
StepHypRef Expression
1 txcn.1 . . . . 5 𝑋 = βˆͺ 𝑅
21toptopon 22410 . . . 4 (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOnβ€˜π‘‹))
3 txcn.2 . . . . 5 π‘Œ = βˆͺ 𝑆
43toptopon 22410 . . . 4 (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOnβ€˜π‘Œ))
5 txcn.5 . . . . . . 7 𝑃 = (1st β†Ύ 𝑍)
6 txcn.3 . . . . . . . 8 𝑍 = (𝑋 Γ— π‘Œ)
76reseq2i 5976 . . . . . . 7 (1st β†Ύ 𝑍) = (1st β†Ύ (𝑋 Γ— π‘Œ))
85, 7eqtri 2760 . . . . . 6 𝑃 = (1st β†Ύ (𝑋 Γ— π‘Œ))
9 tx1cn 23104 . . . . . 6 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ (1st β†Ύ (𝑋 Γ— π‘Œ)) ∈ ((𝑅 Γ—t 𝑆) Cn 𝑅))
108, 9eqeltrid 2837 . . . . 5 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ 𝑃 ∈ ((𝑅 Γ—t 𝑆) Cn 𝑅))
11 txcn.6 . . . . . . 7 𝑄 = (2nd β†Ύ 𝑍)
126reseq2i 5976 . . . . . . 7 (2nd β†Ύ 𝑍) = (2nd β†Ύ (𝑋 Γ— π‘Œ))
1311, 12eqtri 2760 . . . . . 6 𝑄 = (2nd β†Ύ (𝑋 Γ— π‘Œ))
14 tx2cn 23105 . . . . . 6 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ (2nd β†Ύ (𝑋 Γ— π‘Œ)) ∈ ((𝑅 Γ—t 𝑆) Cn 𝑆))
1513, 14eqeltrid 2837 . . . . 5 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ 𝑄 ∈ ((𝑅 Γ—t 𝑆) Cn 𝑆))
16 cnco 22761 . . . . . . 7 ((𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ 𝑃 ∈ ((𝑅 Γ—t 𝑆) Cn 𝑅)) β†’ (𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅))
17 cnco 22761 . . . . . . 7 ((𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ 𝑄 ∈ ((𝑅 Γ—t 𝑆) Cn 𝑆)) β†’ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))
1816, 17anim12dan 619 . . . . . 6 ((𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ (𝑃 ∈ ((𝑅 Γ—t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 Γ—t 𝑆) Cn 𝑆))) β†’ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆)))
1918expcom 414 . . . . 5 ((𝑃 ∈ ((𝑅 Γ—t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 Γ—t 𝑆) Cn 𝑆)) β†’ (𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) β†’ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))))
2010, 15, 19syl2anc 584 . . . 4 ((𝑅 ∈ (TopOnβ€˜π‘‹) ∧ 𝑆 ∈ (TopOnβ€˜π‘Œ)) β†’ (𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) β†’ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))))
212, 4, 20syl2anb 598 . . 3 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) β†’ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))))
22213adant3 1132 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) β†’ (𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) β†’ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))))
23 cntop1 22735 . . . . . . . 8 ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) β†’ π‘ˆ ∈ Top)
2423ad2antrl 726 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ π‘ˆ ∈ Top)
25 txcn.4 . . . . . . . 8 π‘Š = βˆͺ π‘ˆ
2625topopn 22399 . . . . . . 7 (π‘ˆ ∈ Top β†’ π‘Š ∈ π‘ˆ)
2724, 26syl 17 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ π‘Š ∈ π‘ˆ)
2825, 1cnf 22741 . . . . . . 7 ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) β†’ (𝑃 ∘ 𝐹):π‘ŠβŸΆπ‘‹)
2928ad2antrl 726 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ (𝑃 ∘ 𝐹):π‘ŠβŸΆπ‘‹)
3025, 3cnf 22741 . . . . . . 7 ((𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆) β†’ (𝑄 ∘ 𝐹):π‘ŠβŸΆπ‘Œ)
3130ad2antll 727 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ (𝑄 ∘ 𝐹):π‘ŠβŸΆπ‘Œ)
328, 13upxp 23118 . . . . . . 7 ((π‘Š ∈ π‘ˆ ∧ (𝑃 ∘ 𝐹):π‘ŠβŸΆπ‘‹ ∧ (𝑄 ∘ 𝐹):π‘ŠβŸΆπ‘Œ) β†’ βˆƒ!β„Ž(β„Ž:π‘ŠβŸΆ(𝑋 Γ— π‘Œ) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
33 feq3 6697 . . . . . . . . . 10 (𝑍 = (𝑋 Γ— π‘Œ) β†’ (β„Ž:π‘ŠβŸΆπ‘ ↔ β„Ž:π‘ŠβŸΆ(𝑋 Γ— π‘Œ)))
346, 33ax-mp 5 . . . . . . . . 9 (β„Ž:π‘ŠβŸΆπ‘ ↔ β„Ž:π‘ŠβŸΆ(𝑋 Γ— π‘Œ))
35343anbi1i 1157 . . . . . . . 8 ((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ↔ (β„Ž:π‘ŠβŸΆ(𝑋 Γ— π‘Œ) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
3635eubii 2579 . . . . . . 7 (βˆƒ!β„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ↔ βˆƒ!β„Ž(β„Ž:π‘ŠβŸΆ(𝑋 Γ— π‘Œ) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
3732, 36sylibr 233 . . . . . 6 ((π‘Š ∈ π‘ˆ ∧ (𝑃 ∘ 𝐹):π‘ŠβŸΆπ‘‹ ∧ (𝑄 ∘ 𝐹):π‘ŠβŸΆπ‘Œ) β†’ βˆƒ!β„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
3827, 29, 31, 37syl3anc 1371 . . . . 5 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ βˆƒ!β„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
39 euex 2571 . . . . 5 (βˆƒ!β„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) β†’ βˆƒβ„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
4038, 39syl 17 . . . 4 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ βˆƒβ„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
41 simpll3 1214 . . . . . . 7 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) ∧ (β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ 𝐹:π‘ŠβŸΆπ‘)
4227adantr 481 . . . . . . 7 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) ∧ (β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ π‘Š ∈ π‘ˆ)
4341, 42fexd 7225 . . . . . 6 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) ∧ (β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ 𝐹 ∈ V)
44 eumo 2572 . . . . . . . 8 (βˆƒ!β„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) β†’ βˆƒ*β„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
4538, 44syl 17 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ βˆƒ*β„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
4645adantr 481 . . . . . 6 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) ∧ (β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ βˆƒ*β„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
47 simpr 485 . . . . . 6 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) ∧ (β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ (β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
48 3anass 1095 . . . . . . . 8 ((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ↔ (β„Ž:π‘ŠβŸΆπ‘ ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))))
49 coeq2 5856 . . . . . . . . . . . 12 (𝐹 = β„Ž β†’ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž))
50 coeq2 5856 . . . . . . . . . . . 12 (𝐹 = β„Ž β†’ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))
5149, 50jca 512 . . . . . . . . . . 11 (𝐹 = β„Ž β†’ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
5251eqcoms 2740 . . . . . . . . . 10 (β„Ž = 𝐹 β†’ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
5352biantrud 532 . . . . . . . . 9 (β„Ž = 𝐹 β†’ (β„Ž:π‘ŠβŸΆπ‘ ↔ (β„Ž:π‘ŠβŸΆπ‘ ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))))
54 feq1 6695 . . . . . . . . 9 (β„Ž = 𝐹 β†’ (β„Ž:π‘ŠβŸΆπ‘ ↔ 𝐹:π‘ŠβŸΆπ‘))
5553, 54bitr3d 280 . . . . . . . 8 (β„Ž = 𝐹 β†’ ((β„Ž:π‘ŠβŸΆπ‘ ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) ↔ 𝐹:π‘ŠβŸΆπ‘))
5648, 55bitrid 282 . . . . . . 7 (β„Ž = 𝐹 β†’ ((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ↔ 𝐹:π‘ŠβŸΆπ‘))
5756moi2 3711 . . . . . 6 (((𝐹 ∈ V ∧ βˆƒ*β„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) ∧ ((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ∧ 𝐹:π‘ŠβŸΆπ‘)) β†’ β„Ž = 𝐹)
5843, 46, 47, 41, 57syl22anc 837 . . . . 5 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) ∧ (β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ β„Ž = 𝐹)
59 eqid 2732 . . . . . . . . . 10 (𝑅 Γ—t 𝑆) = (𝑅 Γ—t 𝑆)
6059, 1, 3, 6, 5, 11uptx 23120 . . . . . . . . 9 (((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆)) β†’ βˆƒ!β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
6160adantl 482 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ βˆƒ!β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))
62 df-reu 3377 . . . . . . . . . 10 (βˆƒ!β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ↔ βˆƒ!β„Ž(β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))))
63 euex 2571 . . . . . . . . . 10 (βˆƒ!β„Ž(β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ βˆƒβ„Ž(β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))))
6462, 63sylbi 216 . . . . . . . . 9 (βˆƒ!β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) β†’ βˆƒβ„Ž(β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))))
65 eqid 2732 . . . . . . . . . . . . . . 15 βˆͺ (𝑅 Γ—t 𝑆) = βˆͺ (𝑅 Γ—t 𝑆)
6625, 65cnf 22741 . . . . . . . . . . . . . 14 (β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) β†’ β„Ž:π‘ŠβŸΆβˆͺ (𝑅 Γ—t 𝑆))
671, 3txuni 23087 . . . . . . . . . . . . . . . . . 18 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ (𝑋 Γ— π‘Œ) = βˆͺ (𝑅 Γ—t 𝑆))
686, 67eqtrid 2784 . . . . . . . . . . . . . . . . 17 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) β†’ 𝑍 = βˆͺ (𝑅 Γ—t 𝑆))
69683adant3 1132 . . . . . . . . . . . . . . . 16 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) β†’ 𝑍 = βˆͺ (𝑅 Γ—t 𝑆))
7069adantr 481 . . . . . . . . . . . . . . 15 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ 𝑍 = βˆͺ (𝑅 Γ—t 𝑆))
7170feq3d 6701 . . . . . . . . . . . . . 14 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ (β„Ž:π‘ŠβŸΆπ‘ ↔ β„Ž:π‘ŠβŸΆβˆͺ (𝑅 Γ—t 𝑆)))
7266, 71imbitrrid 245 . . . . . . . . . . . . 13 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ (β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) β†’ β„Ž:π‘ŠβŸΆπ‘))
7372anim1d 611 . . . . . . . . . . . 12 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ ((β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ (β„Ž:π‘ŠβŸΆπ‘ ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)))))
7473, 48syl6ibr 251 . . . . . . . . . . 11 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ ((β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ (β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))))
75 simpl 483 . . . . . . . . . . 11 ((β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)))
7674, 75jca2 514 . . . . . . . . . 10 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ ((β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ ((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ∧ β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)))))
7776eximdv 1920 . . . . . . . . 9 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ (βˆƒβ„Ž(β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ βˆƒβ„Ž((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ∧ β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)))))
7864, 77syl5 34 . . . . . . . 8 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ (βˆƒ!β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) β†’ βˆƒβ„Ž((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ∧ β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)))))
7961, 78mpd 15 . . . . . . 7 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ βˆƒβ„Ž((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ∧ β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆))))
80 eupick 2629 . . . . . . 7 ((βˆƒ!β„Ž(β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ∧ βˆƒβ„Ž((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) ∧ β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)))) β†’ ((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) β†’ β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆))))
8138, 79, 80syl2anc 584 . . . . . 6 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ ((β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž)) β†’ β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆))))
8281imp 407 . . . . 5 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) ∧ (β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ β„Ž ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)))
8358, 82eqeltrrd 2834 . . . 4 ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) ∧ (β„Ž:π‘ŠβŸΆπ‘ ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ β„Ž) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ β„Ž))) β†’ 𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)))
8440, 83exlimddv 1938 . . 3 (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) ∧ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))) β†’ 𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)))
8584ex 413 . 2 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) β†’ (((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆)) β†’ 𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆))))
8622, 85impbid 211 1 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:π‘ŠβŸΆπ‘) β†’ (𝐹 ∈ (π‘ˆ Cn (𝑅 Γ—t 𝑆)) ↔ ((𝑃 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (π‘ˆ Cn 𝑆))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106  βˆƒ*wmo 2532  βˆƒ!weu 2562  βˆƒ!wreu 3374  Vcvv 3474  βˆͺ cuni 4907   Γ— cxp 5673   β†Ύ cres 5677   ∘ ccom 5679  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405  1st c1st 7969  2nd c2nd 7970  Topctop 22386  TopOnctopon 22403   Cn ccn 22719   Γ—t ctx 23055
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-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
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-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7971  df-2nd 7972  df-map 8818  df-topgen 17385  df-top 22387  df-topon 22404  df-bases 22440  df-cn 22722  df-tx 23057
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator