Theorem txcn 13442

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.

Step	Hyp	Ref	Expression
1		txcn.1	. . . . 5 ⊢ 𝑋 = ∪ 𝑅
2	1	toptopon 13183	. . . 4 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
3		txcn.2	. . . . 5 ⊢ 𝑌 = ∪ 𝑆
4	3	toptopon 13183	. . . 4 ⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘𝑌))
5		txcn.5	. . . . . . 7 ⊢ 𝑃 = (1st ↾ 𝑍)
6		txcn.3	. . . . . . . 8 ⊢ 𝑍 = (𝑋 × 𝑌)
7	6	reseq2i 4900	. . . . . . 7 ⊢ (1st ↾ 𝑍) = (1st ↾ (𝑋 × 𝑌))
8	5, 7	eqtri 2198	. . . . . 6 ⊢ 𝑃 = (1st ↾ (𝑋 × 𝑌))
9		tx1cn 13436	. . . . . 6 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
10	8, 9	eqeltrid 2264	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
11		txcn.6	. . . . . . 7 ⊢ 𝑄 = (2nd ↾ 𝑍)
12	6	reseq2i 4900	. . . . . . 7 ⊢ (2nd ↾ 𝑍) = (2nd ↾ (𝑋 × 𝑌))
13	11, 12	eqtri 2198	. . . . . 6 ⊢ 𝑄 = (2nd ↾ (𝑋 × 𝑌))
14		tx2cn 13437	. . . . . 6 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
15	13, 14	eqeltrid 2264	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
16		cnco 13388	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ 𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) → (𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅))
17		cnco 13388	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))
18	16, 17	anim12dan 600	. . . . . 6 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ (𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆))) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)))
19	18	expcom 116	. . . . 5 ⊢ ((𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
20	10, 15, 19	syl2anc 411	. . . 4 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
21	2, 4, 20	syl2anb 291	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
22	21	3adant3 1017	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
23		cntop1 13368	. . . . . . . 8 ⊢ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) → 𝑈 ∈ Top)
24	23	ad2antrl 490	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑈 ∈ Top)
25		txcn.4	. . . . . . . 8 ⊢ 𝑊 = ∪ 𝑈
26	25	topopn 13173	. . . . . . 7 ⊢ (𝑈 ∈ Top → 𝑊 ∈ 𝑈)
27	24, 26	syl 14	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑊 ∈ 𝑈)
28	25, 1	cnf 13371	. . . . . . 7 ⊢ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) → (𝑃 ∘ 𝐹):𝑊⟶𝑋)
29	28	ad2antrl 490	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (𝑃 ∘ 𝐹):𝑊⟶𝑋)
30	25, 3	cnf 13371	. . . . . . 7 ⊢ ((𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆) → (𝑄 ∘ 𝐹):𝑊⟶𝑌)
31	30	ad2antll 491	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (𝑄 ∘ 𝐹):𝑊⟶𝑌)
32	8, 13	upxp 13439	. . . . . . 7 ⊢ ((𝑊 ∈ 𝑈 ∧ (𝑃 ∘ 𝐹):𝑊⟶𝑋 ∧ (𝑄 ∘ 𝐹):𝑊⟶𝑌) → ∃!ℎ(ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
33		feq3 5346	. . . . . . . . . 10 ⊢ (𝑍 = (𝑋 × 𝑌) → (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶(𝑋 × 𝑌)))
34	6, 33	ax-mp 5	. . . . . . . . 9 ⊢ (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶(𝑋 × 𝑌))
35	34	3anbi1i 1190	. . . . . . . 8 ⊢ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ (ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
36	35	eubii 2035	. . . . . . 7 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
37	32, 36	sylibr 134	. . . . . 6 ⊢ ((𝑊 ∈ 𝑈 ∧ (𝑃 ∘ 𝐹):𝑊⟶𝑋 ∧ (𝑄 ∘ 𝐹):𝑊⟶𝑌) → ∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
38	27, 29, 31, 37	syl3anc 1238	. . . . 5 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
39		euex 2056	. . . . 5 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
40	38, 39	syl 14	. . . 4 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
41		simpll3 1038	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹:𝑊⟶𝑍)
42	27	adantr 276	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝑊 ∈ 𝑈)
43	1	topopn 13173	. . . . . . . . . 10 ⊢ (𝑅 ∈ Top → 𝑋 ∈ 𝑅)
44	3	topopn 13173	. . . . . . . . . 10 ⊢ (𝑆 ∈ Top → 𝑌 ∈ 𝑆)
45		xpexg 4737	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑆) → (𝑋 × 𝑌) ∈ V)
46	6, 45	eqeltrid 2264	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑆) → 𝑍 ∈ V)
47	43, 44, 46	syl2an 289	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑍 ∈ V)
48	47	3adant3 1017	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → 𝑍 ∈ V)
49	48	ad2antrr 488	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝑍 ∈ V)
50		fex2 5380	. . . . . . 7 ⊢ ((𝐹:𝑊⟶𝑍 ∧ 𝑊 ∈ 𝑈 ∧ 𝑍 ∈ V) → 𝐹 ∈ V)
51	41, 42, 49, 50	syl3anc 1238	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹 ∈ V)
52		eumo 2058	. . . . . . . 8 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
53	38, 52	syl 14	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
54	53	adantr 276	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
55		simpr 110	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
56		3anass 982	. . . . . . . 8 ⊢ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
57		coeq2 4781	. . . . . . . . . . . 12 ⊢ (𝐹 = ℎ → (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ))
58		coeq2 4781	. . . . . . . . . . . 12 ⊢ (𝐹 = ℎ → (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))
59	57, 58	jca 306	. . . . . . . . . . 11 ⊢ (𝐹 = ℎ → ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
60	59	eqcoms 2180	. . . . . . . . . 10 ⊢ (ℎ = 𝐹 → ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
61	60	biantrud 304	. . . . . . . . 9 ⊢ (ℎ = 𝐹 → (ℎ:𝑊⟶𝑍 ↔ (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))))
62		feq1 5344	. . . . . . . . 9 ⊢ (ℎ = 𝐹 → (ℎ:𝑊⟶𝑍 ↔ 𝐹:𝑊⟶𝑍))
63	61, 62	bitr3d 190	. . . . . . . 8 ⊢ (ℎ = 𝐹 → ((ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) ↔ 𝐹:𝑊⟶𝑍))
64	56, 63	bitrid 192	. . . . . . 7 ⊢ (ℎ = 𝐹 → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ 𝐹:𝑊⟶𝑍))
65	64	moi2 2918	. . . . . 6 ⊢ (((𝐹 ∈ V ∧ ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) ∧ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ 𝐹:𝑊⟶𝑍)) → ℎ = 𝐹)
66	51, 54, 55, 41, 65	syl22anc 1239	. . . . 5 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ = 𝐹)
67		eqid 2177	. . . . . . . . . 10 ⊢ (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
68	67, 1, 3, 6, 5, 11	uptx 13441	. . . . . . . . 9 ⊢ (((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)) → ∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
69	68	adantl 277	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
70		df-reu 2462	. . . . . . . . . 10 ⊢ (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
71		euex 2056	. . . . . . . . . 10 ⊢ (∃!ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
72	70, 71	sylbi 121	. . . . . . . . 9 ⊢ (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
73		eqid 2177	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
74	25, 73	cnf 13371	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ℎ:𝑊⟶∪ (𝑅 ×t 𝑆))
75	1, 3	txuni 13430	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆))
76	6, 75	eqtrid 2222	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑍 = ∪ (𝑅 ×t 𝑆))
77	76	3adant3 1017	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → 𝑍 = ∪ (𝑅 ×t 𝑆))
78	77	adantr 276	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑍 = ∪ (𝑅 ×t 𝑆))
79	78	feq3d 5350	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶∪ (𝑅 ×t 𝑆)))
80	74, 79	syl5ibr 156	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ℎ:𝑊⟶𝑍))
81	80	anim1d 336	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))))
82	81, 56	syl6ibr 162	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
83		simpl 109	. . . . . . . . . . 11 ⊢ ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
84	82, 83	jca2 308	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
85	84	eximdv 1880	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
86	72, 85	syl5 32	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
87	69, 86	mpd 13	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
88		eupick 2105	. . . . . . 7 ⊢ ((∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
89	38, 87, 88	syl2anc 411	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
90	89	imp 124	. . . . 5 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
91	66, 90	eqeltrrd 2255	. . . 4 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
92	40, 91	exlimddv 1898	. . 3 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
93	92	ex 115	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
94	22, 93	impbid 129	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ↔ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 978   = wceq 1353  ∃wex 1492  ∃!weu 2026  ∃*wmo 2027   ∈ wcel 2148  ∃!wreu 2457  Vcvv 2737  ∪ cuni 3807   × cxp 4621   ↾ cres 4625   ∘ ccom 4627  ⟶wf 5208  ‘cfv 5212  (class class class)co 5869  1^st c1st 6133  2^nd c2nd 6134  Topctop 13162  TopOnctopon 13175   Cn ccn 13352   ×_t ctx 13419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-map 6644  df-topgen 12657  df-top 13163  df-topon 13176  df-bases 13208  df-cn 13355  df-tx 13420

This theorem is referenced by: (None)