Theorem txcn 21239

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 20548	. . . 4 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
3		txcn.2	. . . . 5 ⊢ 𝑌 = ∪ 𝑆
4	3	toptopon 20548	. . . 4 ⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘𝑌))
5		txcn.5	. . . . . . 7 ⊢ 𝑃 = (1st ↾ 𝑍)
6		txcn.3	. . . . . . . 8 ⊢ 𝑍 = (𝑋 × 𝑌)
7	6	reseq2i 5314	. . . . . . 7 ⊢ (1st ↾ 𝑍) = (1st ↾ (𝑋 × 𝑌))
8	5, 7	eqtri 2632	. . . . . 6 ⊢ 𝑃 = (1st ↾ (𝑋 × 𝑌))
9		tx1cn 21222	. . . . . 6 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
10	8, 9	syl5eqel 2692	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
11		txcn.6	. . . . . . 7 ⊢ 𝑄 = (2nd ↾ 𝑍)
12	6	reseq2i 5314	. . . . . . 7 ⊢ (2nd ↾ 𝑍) = (2nd ↾ (𝑋 × 𝑌))
13	11, 12	eqtri 2632	. . . . . 6 ⊢ 𝑄 = (2nd ↾ (𝑋 × 𝑌))
14		tx2cn 21223	. . . . . 6 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
15	13, 14	syl5eqel 2692	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
16		cnco 20880	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ 𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) → (𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅))
17		cnco 20880	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))
18	16, 17	anim12dan 878	. . . . . 6 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ (𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆))) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)))
19	18	expcom 450	. . . . 5 ⊢ ((𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
20	10, 15, 19	syl2anc 691	. . . 4 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
21	2, 4, 20	syl2anb 495	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
22	21	3adant3 1074	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
23		cntop1 20854	. . . . . . . 8 ⊢ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) → 𝑈 ∈ Top)
24	23	ad2antrl 760	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑈 ∈ Top)
25		txcn.4	. . . . . . . 8 ⊢ 𝑊 = ∪ 𝑈
26	25	topopn 20536	. . . . . . 7 ⊢ (𝑈 ∈ Top → 𝑊 ∈ 𝑈)
27	24, 26	syl 17	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑊 ∈ 𝑈)
28	25, 1	cnf 20860	. . . . . . 7 ⊢ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) → (𝑃 ∘ 𝐹):𝑊⟶𝑋)
29	28	ad2antrl 760	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (𝑃 ∘ 𝐹):𝑊⟶𝑋)
30	25, 3	cnf 20860	. . . . . . 7 ⊢ ((𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆) → (𝑄 ∘ 𝐹):𝑊⟶𝑌)
31	30	ad2antll 761	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (𝑄 ∘ 𝐹):𝑊⟶𝑌)
32	8, 13	upxp 21236	. . . . . . 7 ⊢ ((𝑊 ∈ 𝑈 ∧ (𝑃 ∘ 𝐹):𝑊⟶𝑋 ∧ (𝑄 ∘ 𝐹):𝑊⟶𝑌) → ∃!ℎ(ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
33		feq3 5941	. . . . . . . . . 10 ⊢ (𝑍 = (𝑋 × 𝑌) → (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶(𝑋 × 𝑌)))
34	6, 33	ax-mp 5	. . . . . . . . 9 ⊢ (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶(𝑋 × 𝑌))
35	34	3anbi1i 1246	. . . . . . . 8 ⊢ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ (ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
36	35	eubii 2480	. . . . . . 7 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
37	32, 36	sylibr 223	. . . . . 6 ⊢ ((𝑊 ∈ 𝑈 ∧ (𝑃 ∘ 𝐹):𝑊⟶𝑋 ∧ (𝑄 ∘ 𝐹):𝑊⟶𝑌) → ∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
38	27, 29, 31, 37	syl3anc 1318	. . . . 5 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
39		euex 2482	. . . . 5 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
40	38, 39	syl 17	. . . 4 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
41		simpll3 1095	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹:𝑊⟶𝑍)
42	27	adantr 480	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝑊 ∈ 𝑈)
43	1	topopn 20536	. . . . . . . . . 10 ⊢ (𝑅 ∈ Top → 𝑋 ∈ 𝑅)
44	3	topopn 20536	. . . . . . . . . 10 ⊢ (𝑆 ∈ Top → 𝑌 ∈ 𝑆)
45		xpexg 6858	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑆) → (𝑋 × 𝑌) ∈ V)
46	6, 45	syl5eqel 2692	. . . . . . . . . 10 ⊢ ((𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑆) → 𝑍 ∈ V)
47	43, 44, 46	syl2an 493	. . . . . . . . 9 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑍 ∈ V)
48	47	3adant3 1074	. . . . . . . 8 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → 𝑍 ∈ V)
49	48	ad2antrr 758	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝑍 ∈ V)
50		fex2 7014	. . . . . . 7 ⊢ ((𝐹:𝑊⟶𝑍 ∧ 𝑊 ∈ 𝑈 ∧ 𝑍 ∈ V) → 𝐹 ∈ V)
51	41, 42, 49, 50	syl3anc 1318	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹 ∈ V)
52		eumo 2487	. . . . . . . 8 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
53	38, 52	syl 17	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
54	53	adantr 480	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
55		simpr 476	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
56		3anass 1035	. . . . . . . 8 ⊢ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
57		coeq2 5202	. . . . . . . . . . . 12 ⊢ (𝐹 = ℎ → (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ))
58		coeq2 5202	. . . . . . . . . . . 12 ⊢ (𝐹 = ℎ → (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))
59	57, 58	jca 553	. . . . . . . . . . 11 ⊢ (𝐹 = ℎ → ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
60	59	eqcoms 2618	. . . . . . . . . 10 ⊢ (ℎ = 𝐹 → ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
61	60	biantrud 527	. . . . . . . . 9 ⊢ (ℎ = 𝐹 → (ℎ:𝑊⟶𝑍 ↔ (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))))
62		feq1 5939	. . . . . . . . 9 ⊢ (ℎ = 𝐹 → (ℎ:𝑊⟶𝑍 ↔ 𝐹:𝑊⟶𝑍))
63	61, 62	bitr3d 269	. . . . . . . 8 ⊢ (ℎ = 𝐹 → ((ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) ↔ 𝐹:𝑊⟶𝑍))
64	56, 63	syl5bb 271	. . . . . . 7 ⊢ (ℎ = 𝐹 → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ 𝐹:𝑊⟶𝑍))
65	64	moi2 3354	. . . . . 6 ⊢ (((𝐹 ∈ V ∧ ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) ∧ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ 𝐹:𝑊⟶𝑍)) → ℎ = 𝐹)
66	51, 54, 55, 41, 65	syl22anc 1319	. . . . 5 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ = 𝐹)
67		eqid 2610	. . . . . . . . . 10 ⊢ (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
68	67, 1, 3, 6, 5, 11	uptx 21238	. . . . . . . . 9 ⊢ (((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)) → ∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
69	68	adantl 481	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
70		df-reu 2903	. . . . . . . . . 10 ⊢ (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
71		euex 2482	. . . . . . . . . 10 ⊢ (∃!ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
72	70, 71	sylbi 206	. . . . . . . . 9 ⊢ (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
73		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
74	25, 73	cnf 20860	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ℎ:𝑊⟶∪ (𝑅 ×t 𝑆))
75	1, 3	txuni 21205	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆))
76	6, 75	syl5eq 2656	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑍 = ∪ (𝑅 ×t 𝑆))
77	76	3adant3 1074	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → 𝑍 = ∪ (𝑅 ×t 𝑆))
78	77	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑍 = ∪ (𝑅 ×t 𝑆))
79	78	feq3d 5945	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶∪ (𝑅 ×t 𝑆)))
80	74, 79	syl5ibr 235	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ℎ:𝑊⟶𝑍))
81	80	anim1d 586	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))))
82	81, 56	syl6ibr 241	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
83		simpl 472	. . . . . . . . . . . 12 ⊢ ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
84	83	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
85	82, 84	jcad 554	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
86	85	eximdv 1833	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
87	72, 86	syl5 33	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
88	69, 87	mpd 15	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
89		eupick 2524	. . . . . . 7 ⊢ ((∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
90	38, 88, 89	syl2anc 691	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
91	90	imp 444	. . . . 5 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
92	66, 91	eqeltrrd 2689	. . . 4 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
93	40, 92	exlimddv 1850	. . 3 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
94	93	ex 449	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
95	22, 94	impbid 201	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ↔ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃!weu 2458  ∃*wmo 2459  ∃!wreu 2898  Vcvv 3173  ∪ cuni 4372   × cxp 5036   ↾ cres 5040   ∘ ccom 5042  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  1^st c1st 7057  2^nd c2nd 7058  Topctop 20517  TopOnctopon 20518   Cn ccn 20838   ×_t ctx 21173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1st 7059  df-2nd 7060  df-map 7746  df-topgen 15927  df-top 20521  df-bases 20522  df-topon 20523  df-cn 20841  df-tx 21175

This theorem is referenced by: (None)