Theorem txcn 22685

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 21974	. . . 4 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
3		txcn.2	. . . . 5 ⊢ 𝑌 = ∪ 𝑆
4	3	toptopon 21974	. . . 4 ⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘𝑌))
5		txcn.5	. . . . . . 7 ⊢ 𝑃 = (1st ↾ 𝑍)
6		txcn.3	. . . . . . . 8 ⊢ 𝑍 = (𝑋 × 𝑌)
7	6	reseq2i 5877	. . . . . . 7 ⊢ (1st ↾ 𝑍) = (1st ↾ (𝑋 × 𝑌))
8	5, 7	eqtri 2766	. . . . . 6 ⊢ 𝑃 = (1st ↾ (𝑋 × 𝑌))
9		tx1cn 22668	. . . . . 6 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
10	8, 9	eqeltrid 2843	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
11		txcn.6	. . . . . . 7 ⊢ 𝑄 = (2nd ↾ 𝑍)
12	6	reseq2i 5877	. . . . . . 7 ⊢ (2nd ↾ 𝑍) = (2nd ↾ (𝑋 × 𝑌))
13	11, 12	eqtri 2766	. . . . . 6 ⊢ 𝑄 = (2nd ↾ (𝑋 × 𝑌))
14		tx2cn 22669	. . . . . 6 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
15	13, 14	eqeltrid 2843	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
16		cnco 22325	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ 𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) → (𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅))
17		cnco 22325	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))
18	16, 17	anim12dan 618	. . . . . 6 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ (𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆))) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)))
19	18	expcom 413	. . . . 5 ⊢ ((𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
20	10, 15, 19	syl2anc 583	. . . 4 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
21	2, 4, 20	syl2anb 597	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
22	21	3adant3 1130	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
23		cntop1 22299	. . . . . . . 8 ⊢ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) → 𝑈 ∈ Top)
24	23	ad2antrl 724	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑈 ∈ Top)
25		txcn.4	. . . . . . . 8 ⊢ 𝑊 = ∪ 𝑈
26	25	topopn 21963	. . . . . . 7 ⊢ (𝑈 ∈ Top → 𝑊 ∈ 𝑈)
27	24, 26	syl 17	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑊 ∈ 𝑈)
28	25, 1	cnf 22305	. . . . . . 7 ⊢ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) → (𝑃 ∘ 𝐹):𝑊⟶𝑋)
29	28	ad2antrl 724	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (𝑃 ∘ 𝐹):𝑊⟶𝑋)
30	25, 3	cnf 22305	. . . . . . 7 ⊢ ((𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆) → (𝑄 ∘ 𝐹):𝑊⟶𝑌)
31	30	ad2antll 725	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (𝑄 ∘ 𝐹):𝑊⟶𝑌)
32	8, 13	upxp 22682	. . . . . . 7 ⊢ ((𝑊 ∈ 𝑈 ∧ (𝑃 ∘ 𝐹):𝑊⟶𝑋 ∧ (𝑄 ∘ 𝐹):𝑊⟶𝑌) → ∃!ℎ(ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
33		feq3 6567	. . . . . . . . . 10 ⊢ (𝑍 = (𝑋 × 𝑌) → (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶(𝑋 × 𝑌)))
34	6, 33	ax-mp 5	. . . . . . . . 9 ⊢ (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶(𝑋 × 𝑌))
35	34	3anbi1i 1155	. . . . . . . 8 ⊢ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ (ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
36	35	eubii 2585	. . . . . . 7 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
37	32, 36	sylibr 233	. . . . . 6 ⊢ ((𝑊 ∈ 𝑈 ∧ (𝑃 ∘ 𝐹):𝑊⟶𝑋 ∧ (𝑄 ∘ 𝐹):𝑊⟶𝑌) → ∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
38	27, 29, 31, 37	syl3anc 1369	. . . . 5 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
39		euex 2577	. . . . 5 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
40	38, 39	syl 17	. . . 4 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
41		simpll3 1212	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹:𝑊⟶𝑍)
42	27	adantr 480	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝑊 ∈ 𝑈)
43	41, 42	fexd 7085	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹 ∈ V)
44		eumo 2578	. . . . . . . 8 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
45	38, 44	syl 17	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
46	45	adantr 480	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
47		simpr 484	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
48		3anass 1093	. . . . . . . 8 ⊢ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
49		coeq2 5756	. . . . . . . . . . . 12 ⊢ (𝐹 = ℎ → (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ))
50		coeq2 5756	. . . . . . . . . . . 12 ⊢ (𝐹 = ℎ → (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))
51	49, 50	jca 511	. . . . . . . . . . 11 ⊢ (𝐹 = ℎ → ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
52	51	eqcoms 2746	. . . . . . . . . 10 ⊢ (ℎ = 𝐹 → ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
53	52	biantrud 531	. . . . . . . . 9 ⊢ (ℎ = 𝐹 → (ℎ:𝑊⟶𝑍 ↔ (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))))
54		feq1 6565	. . . . . . . . 9 ⊢ (ℎ = 𝐹 → (ℎ:𝑊⟶𝑍 ↔ 𝐹:𝑊⟶𝑍))
55	53, 54	bitr3d 280	. . . . . . . 8 ⊢ (ℎ = 𝐹 → ((ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) ↔ 𝐹:𝑊⟶𝑍))
56	48, 55	syl5bb 282	. . . . . . 7 ⊢ (ℎ = 𝐹 → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ 𝐹:𝑊⟶𝑍))
57	56	moi2 3646	. . . . . 6 ⊢ (((𝐹 ∈ V ∧ ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) ∧ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ 𝐹:𝑊⟶𝑍)) → ℎ = 𝐹)
58	43, 46, 47, 41, 57	syl22anc 835	. . . . 5 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ = 𝐹)
59		eqid 2738	. . . . . . . . . 10 ⊢ (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
60	59, 1, 3, 6, 5, 11	uptx 22684	. . . . . . . . 9 ⊢ (((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)) → ∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
61	60	adantl 481	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
62		df-reu 3070	. . . . . . . . . 10 ⊢ (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
63		euex 2577	. . . . . . . . . 10 ⊢ (∃!ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
64	62, 63	sylbi 216	. . . . . . . . 9 ⊢ (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
65		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
66	25, 65	cnf 22305	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ℎ:𝑊⟶∪ (𝑅 ×t 𝑆))
67	1, 3	txuni 22651	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆))
68	6, 67	eqtrid 2790	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑍 = ∪ (𝑅 ×t 𝑆))
69	68	3adant3 1130	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → 𝑍 = ∪ (𝑅 ×t 𝑆))
70	69	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑍 = ∪ (𝑅 ×t 𝑆))
71	70	feq3d 6571	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶∪ (𝑅 ×t 𝑆)))
72	66, 71	syl5ibr 245	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ℎ:𝑊⟶𝑍))
73	72	anim1d 610	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))))
74	73, 48	syl6ibr 251	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
75		simpl 482	. . . . . . . . . . 11 ⊢ ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
76	74, 75	jca2 513	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
77	76	eximdv 1921	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
78	64, 77	syl5 34	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
79	61, 78	mpd 15	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
80		eupick 2635	. . . . . . 7 ⊢ ((∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
81	38, 79, 80	syl2anc 583	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
82	81	imp 406	. . . . 5 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
83	58, 82	eqeltrrd 2840	. . . 4 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
84	40, 83	exlimddv 1939	. . 3 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
85	84	ex 412	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
86	22, 85	impbid 211	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ↔ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∃*wmo 2538  ∃!weu 2568  ∃!wreu 3065  Vcvv 3422  ∪ cuni 4836   × cxp 5578   ↾ cres 5582   ∘ ccom 5584  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255  1^st c1st 7802  2^nd c2nd 7803  Topctop 21950  TopOnctopon 21967   Cn ccn 22283   ×_t ctx 22619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1st 7804  df-2nd 7805  df-map 8575  df-topgen 17071  df-top 21951  df-topon 21968  df-bases 22004  df-cn 22286  df-tx 22621

This theorem is referenced by: (None)