Theorem txcn 23853

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 23143	. . . 4 ⊢ (𝑅 ∈ Top ↔ 𝑅 ∈ (TopOn‘𝑋))
3		txcn.2	. . . . 5 ⊢ 𝑌 = ∪ 𝑆
4	3	toptopon 23143	. . . 4 ⊢ (𝑆 ∈ Top ↔ 𝑆 ∈ (TopOn‘𝑌))
5		txcn.5	. . . . . . 7 ⊢ 𝑃 = (1st ↾ 𝑍)
6		txcn.3	. . . . . . . 8 ⊢ 𝑍 = (𝑋 × 𝑌)
7	6	reseq2i 5973	. . . . . . 7 ⊢ (1st ↾ 𝑍) = (1st ↾ (𝑋 × 𝑌))
8	5, 7	eqtri 2785	. . . . . 6 ⊢ 𝑃 = (1st ↾ (𝑋 × 𝑌))
9		tx1cn 23836	. . . . . 6 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (1st ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
10	8, 9	eqeltrid 2866	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅))
11		txcn.6	. . . . . . 7 ⊢ 𝑄 = (2nd ↾ 𝑍)
12	6	reseq2i 5973	. . . . . . 7 ⊢ (2nd ↾ 𝑍) = (2nd ↾ (𝑋 × 𝑌))
13	11, 12	eqtri 2785	. . . . . 6 ⊢ 𝑄 = (2nd ↾ (𝑋 × 𝑌))
14		tx2cn 23837	. . . . . 6 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (2nd ↾ (𝑋 × 𝑌)) ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
15	13, 14	eqeltrid 2866	. . . . 5 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆))
16		cnco 23492	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ 𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅)) → (𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅))
17		cnco 23492	. . . . . . 7 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))
18	16, 17	anim12dan 631	. . . . . 6 ⊢ ((𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ (𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆))) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)))
19	18	expcom 419	. . . . 5 ⊢ ((𝑃 ∈ ((𝑅 ×t 𝑆) Cn 𝑅) ∧ 𝑄 ∈ ((𝑅 ×t 𝑆) Cn 𝑆)) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
20	10, 15, 19	syl2anc 596	. . . 4 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
21	2, 4, 20	syl2anb 610	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
22	21	3adant3 1150	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))
23		cntop1 23466	. . . . . . . 8 ⊢ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) → 𝑈 ∈ Top)
24	23	ad2antrl 741	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑈 ∈ Top)
25		txcn.4	. . . . . . . 8 ⊢ 𝑊 = ∪ 𝑈
26	25	topopn 23132	. . . . . . 7 ⊢ (𝑈 ∈ Top → 𝑊 ∈ 𝑈)
27	24, 26	syl 18	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑊 ∈ 𝑈)
28	25, 1	cnf 23472	. . . . . . 7 ⊢ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) → (𝑃 ∘ 𝐹):𝑊⟶𝑋)
29	28	ad2antrl 741	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (𝑃 ∘ 𝐹):𝑊⟶𝑋)
30	25, 3	cnf 23472	. . . . . . 7 ⊢ ((𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆) → (𝑄 ∘ 𝐹):𝑊⟶𝑌)
31	30	ad2antll 742	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (𝑄 ∘ 𝐹):𝑊⟶𝑌)
32	8, 13	upxp 23850	. . . . . . 7 ⊢ ((𝑊 ∈ 𝑈 ∧ (𝑃 ∘ 𝐹):𝑊⟶𝑋 ∧ (𝑄 ∘ 𝐹):𝑊⟶𝑌) → ∃!ℎ(ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
33		feq3 6686	. . . . . . . . . 10 ⊢ (𝑍 = (𝑋 × 𝑌) → (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶(𝑋 × 𝑌)))
34	6, 33	ax-mp 5	. . . . . . . . 9 ⊢ (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶(𝑋 × 𝑌))
35	34	3anbi1i 1175	. . . . . . . 8 ⊢ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ (ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
36	35	eubii 2612	. . . . . . 7 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ:𝑊⟶(𝑋 × 𝑌) ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
37	32, 36	sylibr 237	. . . . . 6 ⊢ ((𝑊 ∈ 𝑈 ∧ (𝑃 ∘ 𝐹):𝑊⟶𝑋 ∧ (𝑄 ∘ 𝐹):𝑊⟶𝑌) → ∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
38	27, 29, 31, 37	syl3anc 1398	. . . . 5 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
39		euex 2604	. . . . 5 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
40	38, 39	syl 18	. . . 4 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
41		simpll3 1233	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹:𝑊⟶𝑍)
42	27	adantr 486	. . . . . . 7 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝑊 ∈ 𝑈)
43	41, 42	fexd 7229	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹 ∈ V)
44		eumo 2605	. . . . . . . 8 ⊢ (∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
45	38, 44	syl 18	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
46	45	adantr 486	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
47		simpr 490	. . . . . 6 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
48		3anass 1111	. . . . . . . 8 ⊢ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
49		coeq2 5842	. . . . . . . . . . . 12 ⊢ (𝐹 = ℎ → (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ))
50		coeq2 5842	. . . . . . . . . . . 12 ⊢ (𝐹 = ℎ → (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))
51	49, 50	jca 521	. . . . . . . . . . 11 ⊢ (𝐹 = ℎ → ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
52	51	eqcoms 2770	. . . . . . . . . 10 ⊢ (ℎ = 𝐹 → ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
53	52	biantrud 541	. . . . . . . . 9 ⊢ (ℎ = 𝐹 → (ℎ:𝑊⟶𝑍 ↔ (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))))
54		feq1 6684	. . . . . . . . 9 ⊢ (ℎ = 𝐹 → (ℎ:𝑊⟶𝑍 ↔ 𝐹:𝑊⟶𝑍))
55	53, 54	bitr3d 284	. . . . . . . 8 ⊢ (ℎ = 𝐹 → ((ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) ↔ 𝐹:𝑊⟶𝑍))
56	48, 55	bitrid 286	. . . . . . 7 ⊢ (ℎ = 𝐹 → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ 𝐹:𝑊⟶𝑍))
57	56	moi2 3677	. . . . . 6 ⊢ (((𝐹 ∈ V ∧ ∃*ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) ∧ ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ 𝐹:𝑊⟶𝑍)) → ℎ = 𝐹)
58	43, 46, 47, 41, 57	syl22anc 852	. . . . 5 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ = 𝐹)
59		eqid 2762	. . . . . . . . . 10 ⊢ (𝑅 ×t 𝑆) = (𝑅 ×t 𝑆)
60	59, 1, 3, 6, 5, 11	uptx 23852	. . . . . . . . 9 ⊢ (((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)) → ∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
61	60	adantl 487	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))
62		df-reu 3368	. . . . . . . . . 10 ⊢ (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
63		euex 2604	. . . . . . . . . 10 ⊢ (∃!ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
64	62, 63	sylbi 220	. . . . . . . . 9 ⊢ (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
65		eqid 2762	. . . . . . . . . . . . . . 15 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
66	25, 65	cnf 23472	. . . . . . . . . . . . . 14 ⊢ (ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ℎ:𝑊⟶∪ (𝑅 ×t 𝑆))
67	1, 3	txuni 23819	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆))
68	6, 67	eqtrid 2809	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑍 = ∪ (𝑅 ×t 𝑆))
69	68	3adant3 1150	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → 𝑍 = ∪ (𝑅 ×t 𝑆))
70	69	adantr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝑍 = ∪ (𝑅 ×t 𝑆))
71	70	feq3d 6691	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (ℎ:𝑊⟶𝑍 ↔ ℎ:𝑊⟶∪ (𝑅 ×t 𝑆)))
72	66, 71	imbitrrid 249	. . . . . . . . . . . . 13 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) → ℎ:𝑊⟶𝑍))
73	72	anim1d 623	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)))))
74	73, 48	imbitrrdi 255	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))))
75		simpl 488	. . . . . . . . . . 11 ⊢ ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
76	74, 75	jca2 523	. . . . . . . . . 10 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
77	76	eximdv 1950	. . . . . . . . 9 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (∃ℎ(ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ∧ ((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
78	64, 77	syl5 35	. . . . . . . 8 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → (∃!ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))((𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))))
79	61, 78	mpd 16	. . . . . . 7 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
80		eupick 2660	. . . . . . 7 ⊢ ((∃!ℎ(ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ∃ℎ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) ∧ ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
81	38, 79, 80	syl2anc 596	. . . . . 6 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → ((ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ)) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
82	81	imp 412	. . . . 5 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → ℎ ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
83	58, 82	eqeltrrd 2863	. . . 4 ⊢ ((((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) ∧ (ℎ:𝑊⟶𝑍 ∧ (𝑃 ∘ 𝐹) = (𝑃 ∘ ℎ) ∧ (𝑄 ∘ 𝐹) = (𝑄 ∘ ℎ))) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
84	40, 83	exlimddv 1968	. . 3 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) ∧ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
85	84	ex 418	. 2 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆)) → 𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆))))
86	22, 85	impbid 215	1 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹:𝑊⟶𝑍) → (𝐹 ∈ (𝑈 Cn (𝑅 ×t 𝑆)) ↔ ((𝑃 ∘ 𝐹) ∈ (𝑈 Cn 𝑅) ∧ (𝑄 ∘ 𝐹) ∈ (𝑈 Cn 𝑆))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃*wmo 2564  ∃!weu 2595  ∃!wreu 3365  Vcvv 3453  ∪ cuni 4870   × cxp 5657   ↾ cres 5661   ∘ ccom 5663  ⟶wf 6533  ‘cfv 6537  (class class class)co 7416  1^st c1st 7987  2^nd c2nd 7988  Topctop 23119  TopOnctopon 23136   Cn ccn 23450   ×_t ctx 23787

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7989  df-2nd 7990  df-map 8831  df-topgen 17532  df-top 23120  df-topon 23137  df-bases 23172  df-cn 23453  df-tx 23789

This theorem is used by: (None)