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	41 42	fexd	$⊢ (((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$
44		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)$
45	38 44	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)$
46	45	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)$
47		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)$
48		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))$
49		coeq2	$⊢ F = h \to P \circ F = P \circ h$
50		coeq2	$⊢ F = h \to Q \circ F = Q \circ h$
51	49 50	jca	$⊢ F = h \to (P \circ F = P \circ h \land Q \circ F = Q \circ h)$
52	51	eqcoms	$⊢ h = F \to (P \circ F = P \circ h \land Q \circ F = Q \circ h)$
53	52	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)))$
54		feq1	$⊢ h = F \to (h : W ⟶ Z \leftrightarrow F : W ⟶ Z)$
55	53 54	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)$
56	48 55	bitrid	$⊢ h = F \to ((h : W ⟶ Z \land P \circ F = P \circ h \land Q \circ F = Q \circ h) \leftrightarrow F : W ⟶ Z)$
57	56	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$
58	43 46 47 41 57	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$
59		eqid	$⊢ R \times_{t} S = R \times_{t} S$
60	59 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)$
61	60	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)$
62		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))$
63		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))$
64	62 63	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))$
65		eqid	$⊢ ⋃ (R \times_{t} S) = ⋃ (R \times_{t} S)$
66	4 65	cnf	$⊢ h \in (U Cn (R \times_{t} S)) \to h : W ⟶ ⋃ (R \times_{t} S)$
67	1 2	txuni	$⊢ (R \in Top \land S \in Top) \to X \times Y = ⋃ (R \times_{t} S)$
68	3 67	eqtrid	$⊢ (R \in Top \land S \in Top) \to Z = ⋃ (R \times_{t} S)$
69	68	3adant3	$⊢ (R \in Top \land S \in Top \land F : W ⟶ Z) \to Z = ⋃ (R \times_{t} S)$
70	69	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)$
71	70	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))$
72	66 71	imbitrrid	$⊢ ((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)$
73	72	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)))$
74	73 48	imbitrrdi	$⊢ ((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))$
75		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))$
76	74 75	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))))$
77	76	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))))$
78	64 77	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))))$
79	61 78	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)))$
80		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)))$
81	38 79 80	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)))$
82	81	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))$
83	58 82	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))$
84	40 83	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))$
85	84	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)))$
86	23 85	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