txcn

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)

	Ref	Expression
Hypotheses	txcn.1	$⊢ X = ⋃ R$
	txcn.2	$⊢ Y = ⋃ S$
	txcn.3	$⊢ Z = X \times Y$
	txcn.4	$⊢ W = ⋃ U$
	txcn.5	$⊢ P = {1^{st} ↾}_{Z}$
	txcn.6	$⊢ Q = {2^{nd} ↾}_{Z}$
Assertion	txcn	$⊢ (R \in Top \land S \in Top \land F : W ⟶ Z) \to (F \in (U Cn (R \times_{t} S)) \leftrightarrow (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S)))$

Proof

Step	Hyp	Ref	Expression
1		txcn.1	$⊢ X = ⋃ R$
2		txcn.2	$⊢ Y = ⋃ S$
3		txcn.3	$⊢ Z = X \times Y$
4		txcn.4	$⊢ W = ⋃ U$
5		txcn.5	$⊢ P = {1^{st} ↾}_{Z}$
6		txcn.6	$⊢ Q = {2^{nd} ↾}_{Z}$
7	1	toptopon	$⊢ R \in Top \leftrightarrow R \in TopOn (X)$
8	2	toptopon	$⊢ S \in Top \leftrightarrow S \in TopOn (Y)$
9	3	reseq2i	$⊢ {1^{st} ↾}_{Z} = {1^{st} ↾}_{(X \times Y)}$
10	5 9	eqtri	$⊢ P = {1^{st} ↾}_{(X \times Y)}$
11		tx1cn	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to {1^{st} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn R)$
12	10 11	eqeltrid	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to P \in ((R \times_{t} S) Cn R)$
13	3	reseq2i	$⊢ {2^{nd} ↾}_{Z} = {2^{nd} ↾}_{(X \times Y)}$
14	6 13	eqtri	$⊢ Q = {2^{nd} ↾}_{(X \times Y)}$
15		tx2cn	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to {2^{nd} ↾}_{(X \times Y)} \in ((R \times_{t} S) Cn S)$
16	14 15	eqeltrid	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to Q \in ((R \times_{t} S) Cn S)$
17		cnco	$⊢ (F \in (U Cn (R \times_{t} S)) \land P \in ((R \times_{t} S) Cn R)) \to P \circ F \in (U Cn R)$
18		cnco	$⊢ (F \in (U Cn (R \times_{t} S)) \land Q \in ((R \times_{t} S) Cn S)) \to Q \circ F \in (U Cn S)$
19	17 18	anim12dan	$⊢ (F \in (U Cn (R \times_{t} S)) \land (P \in ((R \times_{t} S) Cn R) \land Q \in ((R \times_{t} S) Cn S))) \to (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))$
20	19	expcom	$⊢ (P \in ((R \times_{t} S) Cn R) \land Q \in ((R \times_{t} S) Cn S)) \to (F \in (U Cn (R \times_{t} S)) \to (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S)))$
21	12 16 20	syl2anc	$⊢ (R \in TopOn (X) \land S \in TopOn (Y)) \to (F \in (U Cn (R \times_{t} S)) \to (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S)))$
22	7 8 21	syl2anb	$⊢ (R \in Top \land S \in Top) \to (F \in (U Cn (R \times_{t} S)) \to (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S)))$
23	22	3adant3	$⊢ (R \in Top \land S \in Top \land F : W ⟶ Z) \to (F \in (U Cn (R \times_{t} S)) \to (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S)))$
24		cntop1	$⊢ P \circ F \in (U Cn R) \to U \in Top$
25	24	ad2antrl	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to U \in Top$
26	4	topopn	$⊢ U \in Top \to W \in U$
27	25 26	syl	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to W \in U$
28	4 1	cnf	$⊢ P \circ F \in (U Cn R) \to (P \circ F) : W ⟶ X$
29	28	ad2antrl	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to (P \circ F) : W ⟶ X$
30	4 2	cnf	$⊢ Q \circ F \in (U Cn S) \to (Q \circ F) : W ⟶ Y$
31	30	ad2antll	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to (Q \circ F) : W ⟶ Y$
32	10 14	upxp	$⊢ (W \in U \land (P \circ F) : W ⟶ X \land (Q \circ F) : W ⟶ Y) \to \exists! h (h : W ⟶ X \times Y \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
33		feq3	$⊢ Z = X \times Y \to (h : W ⟶ Z \leftrightarrow h : W ⟶ X \times Y)$
34	3 33	ax-mp	$⊢ h : W ⟶ Z \leftrightarrow h : W ⟶ X \times Y$
35	34	3anbi1i	$⊢ (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \leftrightarrow (h : W ⟶ X \times Y \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
36	35	eubii	$⊢ \exists! h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \leftrightarrow \exists! h (h : W ⟶ X \times Y \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
37	32 36	sylibr	$⊢ (W \in U \land (P \circ F) : W ⟶ X \land (Q \circ F) : W ⟶ Y) \to \exists! h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
38	27 29 31 37	syl3anc	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to \exists! h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
39		euex	$⊢ \exists! h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \to \exists h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
40	38 39	syl	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to \exists h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
41		simpll3	$⊢ (((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \land (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to F : W ⟶ Z$
42	27	adantr	$⊢ (((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \land (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to W \in U$
43	1	topopn	$⊢ R \in Top \to X \in R$
44	2	topopn	$⊢ S \in Top \to Y \in S$
45		xpexg	$⊢ (X \in R \land Y \in S) \to X \times Y \in V$
46	3 45	eqeltrid	$⊢ (X \in R \land Y \in S) \to Z \in V$
47	43 44 46	syl2an	$⊢ (R \in Top \land S \in Top) \to Z \in V$
48	47	3adant3	$⊢ (R \in Top \land S \in Top \land F : W ⟶ Z) \to Z \in V$
49	48	ad2antrr	$⊢ (((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \land (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to Z \in V$
50		fex2	$⊢ (F : W ⟶ Z \land W \in U \land Z \in V) \to F \in V$
51	41 42 49 50	syl3anc	$⊢ (((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \land (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to F \in V$
52		eumo	$⊢ \exists! h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \to \exists^{*} h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
53	38 52	syl	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to \exists^{*} h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
54	53	adantr	$⊢ (((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \land (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to \exists^{*} h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
55		simpr	$⊢ (((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \land (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)$
56		3anass	$⊢ (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \leftrightarrow (h : W ⟶ Z \land (P \circ F = P \circ h \land Q \circ F = Q \circ h))$
57		coeq2	$⊢ F = h \to P \circ F = P \circ h$
58		coeq2	$⊢ F = h \to Q \circ F = Q \circ h$
59	57 58	jca	$⊢ F = h \to (P \circ F = P \circ h \land Q \circ F = Q \circ h)$
60	59	eqcoms	$⊢ h = F \to (P \circ F = P \circ h \land Q \circ F = Q \circ h)$
61	60	biantrud	$⊢ h = F \to (h : W ⟶ Z \leftrightarrow (h : W ⟶ Z \land (P \circ F = P \circ h \land Q \circ F = Q \circ h)))$
62		feq1	$⊢ h = F \to (h : W ⟶ Z \leftrightarrow F : W ⟶ Z)$
63	61 62	bitr3d	$⊢ h = F \to ((h : W ⟶ Z \land (P \circ F = P \circ h \land Q \circ F = Q \circ h)) \leftrightarrow F : W ⟶ Z)$
64	56 63	syl5bb	$⊢ h = F \to ((h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \leftrightarrow F : W ⟶ Z)$
65	64	moi2	$⊢ ((F \in V \land \exists^{*} h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)) \land ((h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \land F : W ⟶ Z)) \to h = F$
66	51 54 55 41 65	syl22anc	$⊢ (((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \land (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to h = F$
67		eqid	$⊢ R \times_{t} S = R \times_{t} S$
68	67 1 2 3 5 6	uptx	$⊢ (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S)) \to \exists! h \in (U Cn (R \times_{t} S)) (P \circ F = P \circ h \land Q \circ F = Q \circ h)$
69	68	adantl	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to \exists! h \in (U Cn (R \times_{t} S)) (P \circ F = P \circ h \land Q \circ F = Q \circ h)$
70		df-reu	$⊢ \exists! h \in (U Cn (R \times_{t} S)) (P \circ F = P \circ h \land Q \circ F = Q \circ h) \leftrightarrow \exists! h (h \in (U Cn (R \times_{t} S)) \land (P \circ F = P \circ h \land Q \circ F = Q \circ h))$
71		euex	$⊢ \exists! h (h \in (U Cn (R \times_{t} S)) \land (P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to \exists h (h \in (U Cn (R \times_{t} S)) \land (P \circ F = P \circ h \land Q \circ F = Q \circ h))$
72	70 71	sylbi	$⊢ \exists! h \in (U Cn (R \times_{t} S)) (P \circ F = P \circ h \land Q \circ F = Q \circ h) \to \exists h (h \in (U Cn (R \times_{t} S)) \land (P \circ F = P \circ h \land Q \circ F = Q \circ h))$
73		eqid	$⊢ ⋃ (R \times_{t} S) = ⋃ (R \times_{t} S)$
74	4 73	cnf	$⊢ h \in (U Cn (R \times_{t} S)) \to h : W ⟶ ⋃ (R \times_{t} S)$
75	1 2	txuni	$⊢ (R \in Top \land S \in Top) \to X \times Y = ⋃ (R \times_{t} S)$
76	3 75	syl5eq	$⊢ (R \in Top \land S \in Top) \to Z = ⋃ (R \times_{t} S)$
77	76	3adant3	$⊢ (R \in Top \land S \in Top \land F : W ⟶ Z) \to Z = ⋃ (R \times_{t} S)$
78	77	adantr	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to Z = ⋃ (R \times_{t} S)$
79	78	feq3d	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to (h : W ⟶ Z \leftrightarrow h : W ⟶ ⋃ (R \times_{t} S))$
80	74 79	syl5ibr	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to (h \in (U Cn (R \times_{t} S)) \to h : W ⟶ Z)$
81	80	anim1d	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to ((h \in (U Cn (R \times_{t} S)) \land (P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to (h : W ⟶ Z \land (P \circ F = P \circ h \land Q \circ F = Q \circ h)))$
82	81 56	syl6ibr	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to ((h \in (U Cn (R \times_{t} S)) \land (P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h))$
83		simpl	$⊢ (h \in (U Cn (R \times_{t} S)) \land (P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to h \in (U Cn (R \times_{t} S))$
84	82 83	jca2	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to ((h \in (U Cn (R \times_{t} S)) \land (P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to ((h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \land h \in (U Cn (R \times_{t} S))))$
85	84	eximdv	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to (\exists h (h \in (U Cn (R \times_{t} S)) \land (P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to \exists h ((h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \land h \in (U Cn (R \times_{t} S))))$
86	72 85	syl5	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to (\exists! h \in (U Cn (R \times_{t} S)) (P \circ F = P \circ h \land Q \circ F = Q \circ h) \to \exists h ((h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \land h \in (U Cn (R \times_{t} S))))$
87	69 86	mpd	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to \exists h ((h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \land h \in (U Cn (R \times_{t} S)))$
88		eupick	$⊢ (\exists! h (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \land \exists h ((h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \land h \in (U Cn (R \times_{t} S)))) \to ((h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \to h \in (U Cn (R \times_{t} S)))$
89	38 87 88	syl2anc	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to ((h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \to h \in (U Cn (R \times_{t} S)))$
90	89	imp	$⊢ (((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \land (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to h \in (U Cn (R \times_{t} S))$
91	66 90	eqeltrrd	$⊢ (((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \land (h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h)) \to F \in (U Cn (R \times_{t} S))$
92	40 91	exlimddv	$⊢ ((R \in Top \land S \in Top \land F : W ⟶ Z) \land (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S))) \to F \in (U Cn (R \times_{t} S))$
93	92	ex	$⊢ (R \in Top \land S \in Top \land F : W ⟶ Z) \to ((P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S)) \to F \in (U Cn (R \times_{t} S)))$
94	23 93	impbid	$⊢ (R \in Top \land S \in Top \land F : W ⟶ Z) \to (F \in (U Cn (R \times_{t} S)) \leftrightarrow (P \circ F \in (U Cn R) \land Q \circ F \in (U Cn S)))$

Metamath Proof Explorer

Theorem txcn

Proof