Theorem txcn 12444

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 12185	. . . 4 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
3		txcn.2	. . . . 5 ⊢ 𝑌 = ∪ 𝑆
4	3	toptopon 12185	. . . 4 ⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘𝑌))
5		txcn.5	. . . . . . 7 ⊢ 𝑃 = (1st ↾ 𝑍)
6		txcn.3	. . . . . . . 8 ⊢ 𝑍 = (𝑋 × 𝑌)
7	6	reseq2i 4816	. . . . . . 7 ⊢ (1st ↾ 𝑍) = (1st ↾ (𝑋 × 𝑌))
8	5, 7	eqtri 2160	. . . . . 6 ⊢ 𝑃 = (1st ↾ (𝑋 × 𝑌))
9		tx1cn 12438	. . . . . 6 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
10	8, 9	eqeltrid 2226	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
11		txcn.6	. . . . . . 7 ⊢ 𝑄 = (2nd ↾ 𝑍)
12	6	reseq2i 4816	. . . . . . 7 ⊢ (2nd ↾ 𝑍) = (2nd ↾ (𝑋 × 𝑌))
13	11, 12	eqtri 2160	. . . . . 6 ⊢ 𝑄 = (2nd ↾ (𝑋 × 𝑌))
14		tx2cn 12439	. . . . . 6 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
15	13, 14	eqeltrid 2226	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
16		cnco 12390	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ 𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) → (𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅))
17		cnco 12390	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))
18	16, 17	anim12dan 589	. . . . . 6 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ (𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆))) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)))
19	18	expcom 115	. . . . 5 ⊢ ((𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
20	10, 15, 19	syl2anc 408	. . . 4 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
21	2, 4, 20	syl2anb 289	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
22	21	3adant3 1001	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
23		cntop1 12370	. . . . . . . 8 ⊢ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) → 𝑈 ∈ Top)
24	23	ad2antrl 481	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑈 ∈ Top)
25		txcn.4	. . . . . . . 8 ⊢ 𝑊 = ∪ 𝑈
26	25	topopn 12175	. . . . . . 7 ⊢ (𝑈 ∈ Top → 𝑊 ∈ 𝑈)
27	24, 26	syl 14	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑊 ∈ 𝑈)
28	25, 1	cnf 12373	. . . . . . 7 ⊢ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) → (𝑃 ∘ 𝐹):𝑊⟶𝑋)
29	28	ad2antrl 481	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (𝑃 ∘ 𝐹):𝑊⟶𝑋)
30	25, 3	cnf 12373	. . . . . . 7 ⊢ ((𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆) → (𝑄 ∘ 𝐹):𝑊⟶𝑌)
31	30	ad2antll 482	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (𝑄 ∘ 𝐹):𝑊⟶𝑌)
32	8, 13	upxp 12441	. . . . . . 7 ⊢ ((𝑊 ∈ 𝑈 ∧ (𝑃 ∘ 𝐹):𝑊⟶𝑋 ∧ (𝑄 ∘ 𝐹):𝑊⟶𝑌) → ∃!ℎ(ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
33		feq3 5257	. . . . . . . . . 10 ⊢ (𝑍 = (𝑋 × 𝑌) → (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶(𝑋 × 𝑌)))
34	6, 33	ax-mp 5	. . . . . . . . 9 ⊢ (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶(𝑋 × 𝑌))
35	34	3anbi1i 1172	. . . . . . . 8 ⊢ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ (ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
36	35	eubii 2008	. . . . . . 7 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
37	32, 36	sylibr 133	. . . . . 6 ⊢ ((𝑊 ∈ 𝑈 ∧ (𝑃 ∘ 𝐹):𝑊⟶𝑋 ∧ (𝑄 ∘ 𝐹):𝑊⟶𝑌) → ∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
38	27, 29, 31, 37	syl3anc 1216	. . . . 5 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
39		euex 2029	. . . . 5 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
40	38, 39	syl 14	. . . 4 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
41		simpll3 1022	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹:𝑊⟶𝑍)
42	27	adantr 274	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝑊 ∈ 𝑈)
43	1	topopn 12175	. . . . . . . . . 10 ⊢ (𝑅 ∈ Top → 𝑋 ∈ 𝑅)
44	3	topopn 12175	. . . . . . . . . 10 ⊢ (𝑆 ∈ Top → 𝑌 ∈ 𝑆)
45		xpexg 4653	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑆) → (𝑋 × 𝑌) ∈ V)
46	6, 45	eqeltrid 2226	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑆) → 𝑍 ∈ V)
47	43, 44, 46	syl2an 287	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑍 ∈ V)
48	47	3adant3 1001	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → 𝑍 ∈ V)
49	48	ad2antrr 479	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝑍 ∈ V)
50		fex2 5291	. . . . . . 7 ⊢ ((𝐹:𝑊⟶𝑍 ∧ 𝑊 ∈ 𝑈 ∧ 𝑍 ∈ V) → 𝐹 ∈ V)
51	41, 42, 49, 50	syl3anc 1216	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹 ∈ V)
52		eumo 2031	. . . . . . . 8 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
53	38, 52	syl 14	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
54	53	adantr 274	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
55		simpr 109	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
56		3anass 966	. . . . . . . 8 ⊢ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
57		coeq2 4697	. . . . . . . . . . . 12 ⊢ (𝐹 = ℎ → (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ))
58		coeq2 4697	. . . . . . . . . . . 12 ⊢ (𝐹 = ℎ → (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))
59	57, 58	jca 304	. . . . . . . . . . 11 ⊢ (𝐹 = ℎ → ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
60	59	eqcoms 2142	. . . . . . . . . 10 ⊢ (ℎ = 𝐹 → ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
61	60	biantrud 302	. . . . . . . . 9 ⊢ (ℎ = 𝐹 → (ℎ:𝑊⟶𝑍 ↔ (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))))
62		feq1 5255	. . . . . . . . 9 ⊢ (ℎ = 𝐹 → (ℎ:𝑊⟶𝑍 ↔ 𝐹:𝑊⟶𝑍))
63	61, 62	bitr3d 189	. . . . . . . 8 ⊢ (ℎ = 𝐹 → ((ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) ↔ 𝐹:𝑊⟶𝑍))
64	56, 63	syl5bb 191	. . . . . . 7 ⊢ (ℎ = 𝐹 → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ 𝐹:𝑊⟶𝑍))
65	64	moi2 2865	. . . . . 6 ⊢ (((𝐹 ∈ V ∧ ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) ∧ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ 𝐹:𝑊⟶𝑍)) → ℎ = 𝐹)
66	51, 54, 55, 41, 65	syl22anc 1217	. . . . 5 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ = 𝐹)
67		eqid 2139	. . . . . . . . . 10 ⊢ (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
68	67, 1, 3, 6, 5, 11	uptx 12443	. . . . . . . . 9 ⊢ (((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)) → ∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
69	68	adantl 275	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
70		df-reu 2423	. . . . . . . . . 10 ⊢ (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
71		euex 2029	. . . . . . . . . 10 ⊢ (∃!ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
72	70, 71	sylbi 120	. . . . . . . . 9 ⊢ (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
73		eqid 2139	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
74	25, 73	cnf 12373	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ℎ:𝑊⟶∪ (𝑅 ×t 𝑆))
75	1, 3	txuni 12432	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆))
76	6, 75	syl5eq 2184	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑍 = ∪ (𝑅 ×t 𝑆))
77	76	3adant3 1001	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → 𝑍 = ∪ (𝑅 ×t 𝑆))
78	77	adantr 274	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑍 = ∪ (𝑅 ×t 𝑆))
79	78	feq3d 5261	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶∪ (𝑅 ×t 𝑆)))
80	74, 79	syl5ibr 155	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ℎ:𝑊⟶𝑍))
81	80	anim1d 334	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))))
82	81, 56	syl6ibr 161	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
83		simpl 108	. . . . . . . . . . 11 ⊢ ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
84	82, 83	jca2 306	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
85	84	eximdv 1852	. . . . . . . . 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 2078	. . . . . . 7 ⊢ ((∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
89	38, 87, 88	syl2anc 408	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
90	89	imp 123	. . . . 5 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
91	66, 90	eqeltrrd 2217	. . . 4 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
92	40, 91	exlimddv 1870	. . 3 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
93	92	ex 114	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
94	22, 93	impbid 128	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ↔ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 962   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∃!weu 1999  ∃*wmo 2000  ∃!wreu 2418  Vcvv 2686  ∪ cuni 3736   × cxp 4537   ↾ cres 4541   ∘ ccom 4543  ⟶wf 5119  ‘cfv 5123  (class class class)co 5774  1^st c1st 6036  2^nd c2nd 6037  Topctop 12164  TopOnctopon 12177   Cn ccn 12354   ×_t ctx 12421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-id 4215  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-map 6544  df-topgen 12141  df-top 12165  df-topon 12178  df-bases 12210  df-cn 12357  df-tx 12422

This theorem is referenced by: (None)