txcnmpt

Description: A map into the product of two topological spaces is continuous if both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	txcnmpt.1	$⊢ W = ⋃ U$
	txcnmpt.2	$⊢ H = (x \in W ⟼ ⟨F (x), G (x)⟩)$
Assertion	txcnmpt	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to H \in (U Cn (R \times_{t} S))$

Proof

Step	Hyp	Ref	Expression
1		txcnmpt.1	$⊢ W = ⋃ U$
2		txcnmpt.2	$⊢ H = (x \in W ⟼ ⟨F (x), G (x)⟩)$
3		eqid	$⊢ ⋃ R = ⋃ R$
4	1 3	cnf	$⊢ F \in (U Cn R) \to F : W ⟶ ⋃ R$
5	4	adantr	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to F : W ⟶ ⋃ R$
6	5	ffvelrnda	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land x \in W) \to F (x) \in ⋃ R$
7		eqid	$⊢ ⋃ S = ⋃ S$
8	1 7	cnf	$⊢ G \in (U Cn S) \to G : W ⟶ ⋃ S$
9	8	adantl	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to G : W ⟶ ⋃ S$
10	9	ffvelrnda	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land x \in W) \to G (x) \in ⋃ S$
11	6 10	opelxpd	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land x \in W) \to ⟨F (x), G (x)⟩ \in (⋃ R \times ⋃ S)$
12	11 2	fmptd	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to H : W ⟶ ⋃ R \times ⋃ S$
13	2	mptpreima	$⊢ H^{-1} [r \times s] = \{x \in W \| ⟨F (x), G (x)⟩ \in (r \times s)\}$
14	5	adantr	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to F : W ⟶ ⋃ R$
15	14	adantr	$⊢ (((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \land x \in W) \to F : W ⟶ ⋃ R$
16		ffn	$⊢ F : W ⟶ ⋃ R \to F Fn W$
17		elpreima	$⊢ F Fn W \to (x \in F^{-1} [r] \leftrightarrow (x \in W \land F (x) \in r))$
18	15 16 17	3syl	$⊢ (((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \land x \in W) \to (x \in F^{-1} [r] \leftrightarrow (x \in W \land F (x) \in r))$
19		ibar	$⊢ x \in W \to (F (x) \in r \leftrightarrow (x \in W \land F (x) \in r))$
20	19	adantl	$⊢ (((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \land x \in W) \to (F (x) \in r \leftrightarrow (x \in W \land F (x) \in r))$
21	18 20	bitr4d	$⊢ (((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \land x \in W) \to (x \in F^{-1} [r] \leftrightarrow F (x) \in r)$
22	9	ad2antrr	$⊢ (((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \land x \in W) \to G : W ⟶ ⋃ S$
23		ffn	$⊢ G : W ⟶ ⋃ S \to G Fn W$
24		elpreima	$⊢ G Fn W \to (x \in G^{-1} [s] \leftrightarrow (x \in W \land G (x) \in s))$
25	22 23 24	3syl	$⊢ (((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \land x \in W) \to (x \in G^{-1} [s] \leftrightarrow (x \in W \land G (x) \in s))$
26		ibar	$⊢ x \in W \to (G (x) \in s \leftrightarrow (x \in W \land G (x) \in s))$
27	26	adantl	$⊢ (((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \land x \in W) \to (G (x) \in s \leftrightarrow (x \in W \land G (x) \in s))$
28	25 27	bitr4d	$⊢ (((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \land x \in W) \to (x \in G^{-1} [s] \leftrightarrow G (x) \in s)$
29	21 28	anbi12d	$⊢ (((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \land x \in W) \to ((x \in F^{-1} [r] \land x \in G^{-1} [s]) \leftrightarrow (F (x) \in r \land G (x) \in s))$
30		elin	$⊢ x \in (F^{-1} [r] \cap G^{-1} [s]) \leftrightarrow (x \in F^{-1} [r] \land x \in G^{-1} [s])$
31		opelxp	$⊢ ⟨F (x), G (x)⟩ \in (r \times s) \leftrightarrow (F (x) \in r \land G (x) \in s)$
32	29 30 31	3bitr4g	$⊢ (((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \land x \in W) \to (x \in (F^{-1} [r] \cap G^{-1} [s]) \leftrightarrow ⟨F (x), G (x)⟩ \in (r \times s))$
33	32	rabbi2dva	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to W \cap (F^{-1} [r] \cap G^{-1} [s]) = \{x \in W \| ⟨F (x), G (x)⟩ \in (r \times s)\}$
34		inss1	$⊢ F^{-1} [r] \cap G^{-1} [s] \subseteq F^{-1} [r]$
35		cnvimass	$⊢ F^{-1} [r] \subseteq dom F$
36	34 35	sstri	$⊢ F^{-1} [r] \cap G^{-1} [s] \subseteq dom F$
37	36 14	fssdm	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to F^{-1} [r] \cap G^{-1} [s] \subseteq W$
38		sseqin2	$⊢ F^{-1} [r] \cap G^{-1} [s] \subseteq W \leftrightarrow W \cap (F^{-1} [r] \cap G^{-1} [s]) = F^{-1} [r] \cap G^{-1} [s]$
39	37 38	sylib	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to W \cap (F^{-1} [r] \cap G^{-1} [s]) = F^{-1} [r] \cap G^{-1} [s]$
40	33 39	eqtr3d	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to \{x \in W \| ⟨F (x), G (x)⟩ \in (r \times s)\} = F^{-1} [r] \cap G^{-1} [s]$
41	13 40	syl5eq	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to H^{-1} [r \times s] = F^{-1} [r] \cap G^{-1} [s]$
42		cntop1	$⊢ G \in (U Cn S) \to U \in Top$
43	42	adantl	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to U \in Top$
44	43	adantr	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to U \in Top$
45		cnima	$⊢ (F \in (U Cn R) \land r \in R) \to F^{-1} [r] \in U$
46	45	ad2ant2r	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to F^{-1} [r] \in U$
47		cnima	$⊢ (G \in (U Cn S) \land s \in S) \to G^{-1} [s] \in U$
48	47	ad2ant2l	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to G^{-1} [s] \in U$
49		inopn	$⊢ (U \in Top \land F^{-1} [r] \in U \land G^{-1} [s] \in U) \to F^{-1} [r] \cap G^{-1} [s] \in U$
50	44 46 48 49	syl3anc	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to F^{-1} [r] \cap G^{-1} [s] \in U$
51	41 50	eqeltrd	$⊢ ((F \in (U Cn R) \land G \in (U Cn S)) \land (r \in R \land s \in S)) \to H^{-1} [r \times s] \in U$
52	51	ralrimivva	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to \forall r \in R \forall s \in S H^{-1} [r \times s] \in U$
53		vex	$⊢ r \in V$
54		vex	$⊢ s \in V$
55	53 54	xpex	$⊢ r \times s \in V$
56	55	rgen2w	$⊢ \forall r \in R \forall s \in S r \times s \in V$
57		eqid	$⊢ (r \in R, s \in S ⟼ r \times s) = (r \in R, s \in S ⟼ r \times s)$
58		imaeq2	$⊢ z = r \times s \to H^{-1} [z] = H^{-1} [r \times s]$
59	58	eleq1d	$⊢ z = r \times s \to (H^{-1} [z] \in U \leftrightarrow H^{-1} [r \times s] \in U)$
60	57 59	ralrnmpo	$⊢ \forall r \in R \forall s \in S r \times s \in V \to (\forall z \in ran (r \in R, s \in S ⟼ r \times s) H^{-1} [z] \in U \leftrightarrow \forall r \in R \forall s \in S H^{-1} [r \times s] \in U)$
61	56 60	ax-mp	$⊢ \forall z \in ran (r \in R, s \in S ⟼ r \times s) H^{-1} [z] \in U \leftrightarrow \forall r \in R \forall s \in S H^{-1} [r \times s] \in U$
62	52 61	sylibr	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to \forall z \in ran (r \in R, s \in S ⟼ r \times s) H^{-1} [z] \in U$
63	1	toptopon	$⊢ U \in Top \leftrightarrow U \in TopOn (W)$
64	43 63	sylib	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to U \in TopOn (W)$
65		cntop2	$⊢ F \in (U Cn R) \to R \in Top$
66		cntop2	$⊢ G \in (U Cn S) \to S \in Top$
67		eqid	$⊢ ran (r \in R, s \in S ⟼ r \times s) = ran (r \in R, s \in S ⟼ r \times s)$
68	67	txval	$⊢ (R \in Top \land S \in Top) \to R \times_{t} S = topGen (ran (r \in R, s \in S ⟼ r \times s))$
69	65 66 68	syl2an	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to R \times_{t} S = topGen (ran (r \in R, s \in S ⟼ r \times s))$
70		toptopon2	$⊢ R \in Top \leftrightarrow R \in TopOn (⋃ R)$
71	65 70	sylib	$⊢ F \in (U Cn R) \to R \in TopOn (⋃ R)$
72		toptopon2	$⊢ S \in Top \leftrightarrow S \in TopOn (⋃ S)$
73	66 72	sylib	$⊢ G \in (U Cn S) \to S \in TopOn (⋃ S)$
74		txtopon	$⊢ (R \in TopOn (⋃ R) \land S \in TopOn (⋃ S)) \to R \times_{t} S \in TopOn (⋃ R \times ⋃ S)$
75	71 73 74	syl2an	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to R \times_{t} S \in TopOn (⋃ R \times ⋃ S)$
76	64 69 75	tgcn	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to (H \in (U Cn (R \times_{t} S)) \leftrightarrow (H : W ⟶ ⋃ R \times ⋃ S \land \forall z \in ran (r \in R, s \in S ⟼ r \times s) H^{-1} [z] \in U))$
77	12 62 76	mpbir2and	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to H \in (U Cn (R \times_{t} S))$

Metamath Proof Explorer

Theorem txcnmpt

Proof