txcnp

Description: If two functions are continuous at D , then the ordered pair of them is continuous at D into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	txcnp.4	$⊢ φ \to J \in TopOn (X)$
	txcnp.5	$⊢ φ \to K \in TopOn (Y)$
	txcnp.6	$⊢ φ \to L \in TopOn (Z)$
	txcnp.7	$⊢ φ \to D \in X$
	txcnp.8	$⊢ φ \to (x \in X ⟼ A) \in (J CnP K) (D)$
	txcnp.9	$⊢ φ \to (x \in X ⟼ B) \in (J CnP L) (D)$
Assertion	txcnp	$⊢ φ \to (x \in X ⟼ ⟨A, B⟩) \in (J CnP (K \times_{t} L)) (D)$

Proof

Step	Hyp	Ref	Expression
1		txcnp.4	$⊢ φ \to J \in TopOn (X)$
2		txcnp.5	$⊢ φ \to K \in TopOn (Y)$
3		txcnp.6	$⊢ φ \to L \in TopOn (Z)$
4		txcnp.7	$⊢ φ \to D \in X$
5		txcnp.8	$⊢ φ \to (x \in X ⟼ A) \in (J CnP K) (D)$
6		txcnp.9	$⊢ φ \to (x \in X ⟼ B) \in (J CnP L) (D)$
7		cnpf2	$⊢ (J \in TopOn (X) \land K \in TopOn (Y) \land (x \in X ⟼ A) \in (J CnP K) (D)) \to (x \in X ⟼ A) : X ⟶ Y$
8	1 2 5 7	syl3anc	$⊢ φ \to (x \in X ⟼ A) : X ⟶ Y$
9	8	fvmptelcdm	$⊢ (φ \land x \in X) \to A \in Y$
10		cnpf2	$⊢ (J \in TopOn (X) \land L \in TopOn (Z) \land (x \in X ⟼ B) \in (J CnP L) (D)) \to (x \in X ⟼ B) : X ⟶ Z$
11	1 3 6 10	syl3anc	$⊢ φ \to (x \in X ⟼ B) : X ⟶ Z$
12	11	fvmptelcdm	$⊢ (φ \land x \in X) \to B \in Z$
13	9 12	opelxpd	$⊢ (φ \land x \in X) \to ⟨A, B⟩ \in (Y \times Z)$
14	13	fmpttd	$⊢ φ \to (x \in X ⟼ ⟨A, B⟩) : X ⟶ Y \times Z$
15		simpr	$⊢ (φ \land x \in X) \to x \in X$
16		opex	$⊢ ⟨A, B⟩ \in V$
17		eqid	$⊢ (x \in X ⟼ ⟨A, B⟩) = (x \in X ⟼ ⟨A, B⟩)$
18	17	fvmpt2	$⊢ (x \in X \land ⟨A, B⟩ \in V) \to (x \in X ⟼ ⟨A, B⟩) (x) = ⟨A, B⟩$
19	15 16 18	sylancl	$⊢ (φ \land x \in X) \to (x \in X ⟼ ⟨A, B⟩) (x) = ⟨A, B⟩$
20		eqid	$⊢ (x \in X ⟼ A) = (x \in X ⟼ A)$
21	20	fvmpt2	$⊢ (x \in X \land A \in Y) \to (x \in X ⟼ A) (x) = A$
22	15 9 21	syl2anc	$⊢ (φ \land x \in X) \to (x \in X ⟼ A) (x) = A$
23		eqid	$⊢ (x \in X ⟼ B) = (x \in X ⟼ B)$
24	23	fvmpt2	$⊢ (x \in X \land B \in Z) \to (x \in X ⟼ B) (x) = B$
25	15 12 24	syl2anc	$⊢ (φ \land x \in X) \to (x \in X ⟼ B) (x) = B$
26	22 25	opeq12d	$⊢ (φ \land x \in X) \to ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩ = ⟨A, B⟩$
27	19 26	eqtr4d	$⊢ (φ \land x \in X) \to (x \in X ⟼ ⟨A, B⟩) (x) = ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩$
28	27	ralrimiva	$⊢ φ \to \forall x \in X (x \in X ⟼ ⟨A, B⟩) (x) = ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩$
29		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ ⟨A, B⟩) (D)$
30		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ A) (D)$
31		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ B) (D)$
32	30 31	nfop	$⊢ \underline{Ⅎ} x ⟨(x \in X ⟼ A) (D), (x \in X ⟼ B) (D)⟩$
33	29 32	nfeq	$⊢ Ⅎ x (x \in X ⟼ ⟨A, B⟩) (D) = ⟨(x \in X ⟼ A) (D), (x \in X ⟼ B) (D)⟩$
34		fveq2	$⊢ x = D \to (x \in X ⟼ ⟨A, B⟩) (x) = (x \in X ⟼ ⟨A, B⟩) (D)$
35		fveq2	$⊢ x = D \to (x \in X ⟼ A) (x) = (x \in X ⟼ A) (D)$
36		fveq2	$⊢ x = D \to (x \in X ⟼ B) (x) = (x \in X ⟼ B) (D)$
37	35 36	opeq12d	$⊢ x = D \to ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩ = ⟨(x \in X ⟼ A) (D), (x \in X ⟼ B) (D)⟩$
38	34 37	eqeq12d	$⊢ x = D \to ((x \in X ⟼ ⟨A, B⟩) (x) = ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩ \leftrightarrow (x \in X ⟼ ⟨A, B⟩) (D) = ⟨(x \in X ⟼ A) (D), (x \in X ⟼ B) (D)⟩)$
39	33 38	rspc	$⊢ D \in X \to (\forall x \in X (x \in X ⟼ ⟨A, B⟩) (x) = ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩ \to (x \in X ⟼ ⟨A, B⟩) (D) = ⟨(x \in X ⟼ A) (D), (x \in X ⟼ B) (D)⟩)$
40	4 28 39	sylc	$⊢ φ \to (x \in X ⟼ ⟨A, B⟩) (D) = ⟨(x \in X ⟼ A) (D), (x \in X ⟼ B) (D)⟩$
41	40	eleq1d	$⊢ φ \to ((x \in X ⟼ ⟨A, B⟩) (D) \in (v \times w) \leftrightarrow ⟨(x \in X ⟼ A) (D), (x \in X ⟼ B) (D)⟩ \in (v \times w))$
42	41	adantr	$⊢ (φ \land (v \in K \land w \in L)) \to ((x \in X ⟼ ⟨A, B⟩) (D) \in (v \times w) \leftrightarrow ⟨(x \in X ⟼ A) (D), (x \in X ⟼ B) (D)⟩ \in (v \times w))$
43	5	ad2antrr	$⊢ ((φ \land (v \in K \land w \in L)) \land ((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w)) \to (x \in X ⟼ A) \in (J CnP K) (D)$
44		simplrl	$⊢ ((φ \land (v \in K \land w \in L)) \land ((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w)) \to v \in K$
45		simprl	$⊢ ((φ \land (v \in K \land w \in L)) \land ((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w)) \to (x \in X ⟼ A) (D) \in v$
46		cnpimaex	$⊢ ((x \in X ⟼ A) \in (J CnP K) (D) \land v \in K \land (x \in X ⟼ A) (D) \in v) \to \exists r \in J (D \in r \land (x \in X ⟼ A) [r] \subseteq v)$
47	43 44 45 46	syl3anc	$⊢ ((φ \land (v \in K \land w \in L)) \land ((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w)) \to \exists r \in J (D \in r \land (x \in X ⟼ A) [r] \subseteq v)$
48	6	ad2antrr	$⊢ ((φ \land (v \in K \land w \in L)) \land ((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w)) \to (x \in X ⟼ B) \in (J CnP L) (D)$
49		simplrr	$⊢ ((φ \land (v \in K \land w \in L)) \land ((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w)) \to w \in L$
50		simprr	$⊢ ((φ \land (v \in K \land w \in L)) \land ((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w)) \to (x \in X ⟼ B) (D) \in w$
51		cnpimaex	$⊢ ((x \in X ⟼ B) \in (J CnP L) (D) \land w \in L \land (x \in X ⟼ B) (D) \in w) \to \exists s \in J (D \in s \land (x \in X ⟼ B) [s] \subseteq w)$
52	48 49 50 51	syl3anc	$⊢ ((φ \land (v \in K \land w \in L)) \land ((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w)) \to \exists s \in J (D \in s \land (x \in X ⟼ B) [s] \subseteq w)$
53	47 52	jca	$⊢ ((φ \land (v \in K \land w \in L)) \land ((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w)) \to (\exists r \in J (D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land \exists s \in J (D \in s \land (x \in X ⟼ B) [s] \subseteq w))$
54	53	ex	$⊢ (φ \land (v \in K \land w \in L)) \to (((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w) \to (\exists r \in J (D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land \exists s \in J (D \in s \land (x \in X ⟼ B) [s] \subseteq w)))$
55		opelxp	$⊢ ⟨(x \in X ⟼ A) (D), (x \in X ⟼ B) (D)⟩ \in (v \times w) \leftrightarrow ((x \in X ⟼ A) (D) \in v \land (x \in X ⟼ B) (D) \in w)$
56		reeanv	$⊢ \exists r \in J \exists s \in J ((D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land (D \in s \land (x \in X ⟼ B) [s] \subseteq w)) \leftrightarrow (\exists r \in J (D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land \exists s \in J (D \in s \land (x \in X ⟼ B) [s] \subseteq w))$
57	54 55 56	3imtr4g	$⊢ (φ \land (v \in K \land w \in L)) \to (⟨(x \in X ⟼ A) (D), (x \in X ⟼ B) (D)⟩ \in (v \times w) \to \exists r \in J \exists s \in J ((D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land (D \in s \land (x \in X ⟼ B) [s] \subseteq w)))$
58	42 57	sylbid	$⊢ (φ \land (v \in K \land w \in L)) \to ((x \in X ⟼ ⟨A, B⟩) (D) \in (v \times w) \to \exists r \in J \exists s \in J ((D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land (D \in s \land (x \in X ⟼ B) [s] \subseteq w)))$
59		an4	$⊢ ((D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land (D \in s \land (x \in X ⟼ B) [s] \subseteq w)) \leftrightarrow ((D \in r \land D \in s) \land ((x \in X ⟼ A) [r] \subseteq v \land (x \in X ⟼ B) [s] \subseteq w))$
60		elin	$⊢ D \in (r \cap s) \leftrightarrow (D \in r \land D \in s)$
61	60	biimpri	$⊢ (D \in r \land D \in s) \to D \in (r \cap s)$
62	61	a1i	$⊢ ((φ \land (v \in K \land w \in L)) \land (r \in J \land s \in J)) \to ((D \in r \land D \in s) \to D \in (r \cap s))$
63		simpl	$⊢ (r \in J \land s \in J) \to r \in J$
64		toponss	$⊢ (J \in TopOn (X) \land r \in J) \to r \subseteq X$
65	1 63 64	syl2an	$⊢ (φ \land (r \in J \land s \in J)) \to r \subseteq X$
66		ssinss1	$⊢ r \subseteq X \to r \cap s \subseteq X$
67	66	adantl	$⊢ (φ \land r \subseteq X) \to r \cap s \subseteq X$
68	67	sselda	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to t \in X$
69	28	ad2antrr	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to \forall x \in X (x \in X ⟼ ⟨A, B⟩) (x) = ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩$
70		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ ⟨A, B⟩) (t)$
71		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ A) (t)$
72		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in X ⟼ B) (t)$
73	71 72	nfop	$⊢ \underline{Ⅎ} x ⟨(x \in X ⟼ A) (t), (x \in X ⟼ B) (t)⟩$
74	70 73	nfeq	$⊢ Ⅎ x (x \in X ⟼ ⟨A, B⟩) (t) = ⟨(x \in X ⟼ A) (t), (x \in X ⟼ B) (t)⟩$
75		fveq2	$⊢ x = t \to (x \in X ⟼ ⟨A, B⟩) (x) = (x \in X ⟼ ⟨A, B⟩) (t)$
76		fveq2	$⊢ x = t \to (x \in X ⟼ A) (x) = (x \in X ⟼ A) (t)$
77		fveq2	$⊢ x = t \to (x \in X ⟼ B) (x) = (x \in X ⟼ B) (t)$
78	76 77	opeq12d	$⊢ x = t \to ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩ = ⟨(x \in X ⟼ A) (t), (x \in X ⟼ B) (t)⟩$
79	75 78	eqeq12d	$⊢ x = t \to ((x \in X ⟼ ⟨A, B⟩) (x) = ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩ \leftrightarrow (x \in X ⟼ ⟨A, B⟩) (t) = ⟨(x \in X ⟼ A) (t), (x \in X ⟼ B) (t)⟩)$
80	74 79	rspc	$⊢ t \in X \to (\forall x \in X (x \in X ⟼ ⟨A, B⟩) (x) = ⟨(x \in X ⟼ A) (x), (x \in X ⟼ B) (x)⟩ \to (x \in X ⟼ ⟨A, B⟩) (t) = ⟨(x \in X ⟼ A) (t), (x \in X ⟼ B) (t)⟩)$
81	68 69 80	sylc	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to (x \in X ⟼ ⟨A, B⟩) (t) = ⟨(x \in X ⟼ A) (t), (x \in X ⟼ B) (t)⟩$
82		simpr	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to t \in (r \cap s)$
83	82	elin1d	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to t \in r$
84	8	ad2antrr	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to (x \in X ⟼ A) : X ⟶ Y$
85	84	ffund	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to Fun (x \in X ⟼ A)$
86	67	adantr	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to r \cap s \subseteq X$
87	84	fdmd	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to dom (x \in X ⟼ A) = X$
88	86 87	sseqtrrd	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to r \cap s \subseteq dom (x \in X ⟼ A)$
89	88 82	sseldd	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to t \in dom (x \in X ⟼ A)$
90		funfvima	$⊢ (Fun (x \in X ⟼ A) \land t \in dom (x \in X ⟼ A)) \to (t \in r \to (x \in X ⟼ A) (t) \in (x \in X ⟼ A) [r])$
91	85 89 90	syl2anc	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to (t \in r \to (x \in X ⟼ A) (t) \in (x \in X ⟼ A) [r])$
92	83 91	mpd	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to (x \in X ⟼ A) (t) \in (x \in X ⟼ A) [r]$
93	82	elin2d	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to t \in s$
94	11	ad2antrr	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to (x \in X ⟼ B) : X ⟶ Z$
95	94	ffund	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to Fun (x \in X ⟼ B)$
96	94	fdmd	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to dom (x \in X ⟼ B) = X$
97	86 96	sseqtrrd	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to r \cap s \subseteq dom (x \in X ⟼ B)$
98	97 82	sseldd	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to t \in dom (x \in X ⟼ B)$
99		funfvima	$⊢ (Fun (x \in X ⟼ B) \land t \in dom (x \in X ⟼ B)) \to (t \in s \to (x \in X ⟼ B) (t) \in (x \in X ⟼ B) [s])$
100	95 98 99	syl2anc	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to (t \in s \to (x \in X ⟼ B) (t) \in (x \in X ⟼ B) [s])$
101	93 100	mpd	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to (x \in X ⟼ B) (t) \in (x \in X ⟼ B) [s]$
102	92 101	opelxpd	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to ⟨(x \in X ⟼ A) (t), (x \in X ⟼ B) (t)⟩ \in ((x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s])$
103	81 102	eqeltrd	$⊢ ((φ \land r \subseteq X) \land t \in (r \cap s)) \to (x \in X ⟼ ⟨A, B⟩) (t) \in ((x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s])$
104	103	ralrimiva	$⊢ (φ \land r \subseteq X) \to \forall t \in (r \cap s) (x \in X ⟼ ⟨A, B⟩) (t) \in ((x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s])$
105	14	ffund	$⊢ φ \to Fun (x \in X ⟼ ⟨A, B⟩)$
106	105	adantr	$⊢ (φ \land r \subseteq X) \to Fun (x \in X ⟼ ⟨A, B⟩)$
107	14	fdmd	$⊢ φ \to dom (x \in X ⟼ ⟨A, B⟩) = X$
108	107	adantr	$⊢ (φ \land r \subseteq X) \to dom (x \in X ⟼ ⟨A, B⟩) = X$
109	67 108	sseqtrrd	$⊢ (φ \land r \subseteq X) \to r \cap s \subseteq dom (x \in X ⟼ ⟨A, B⟩)$
110		funimass4	$⊢ (Fun (x \in X ⟼ ⟨A, B⟩) \land r \cap s \subseteq dom (x \in X ⟼ ⟨A, B⟩)) \to ((x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq (x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s] \leftrightarrow \forall t \in (r \cap s) (x \in X ⟼ ⟨A, B⟩) (t) \in ((x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s]))$
111	106 109 110	syl2anc	$⊢ (φ \land r \subseteq X) \to ((x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq (x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s] \leftrightarrow \forall t \in (r \cap s) (x \in X ⟼ ⟨A, B⟩) (t) \in ((x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s]))$
112	104 111	mpbird	$⊢ (φ \land r \subseteq X) \to (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq (x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s]$
113	65 112	syldan	$⊢ (φ \land (r \in J \land s \in J)) \to (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq (x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s]$
114	113	adantlr	$⊢ ((φ \land (v \in K \land w \in L)) \land (r \in J \land s \in J)) \to (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq (x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s]$
115		xpss12	$⊢ ((x \in X ⟼ A) [r] \subseteq v \land (x \in X ⟼ B) [s] \subseteq w) \to (x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s] \subseteq v \times w$
116		sstr2	$⊢ (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq (x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s] \to ((x \in X ⟼ A) [r] \times (x \in X ⟼ B) [s] \subseteq v \times w \to (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq v \times w)$
117	114 115 116	syl2im	$⊢ ((φ \land (v \in K \land w \in L)) \land (r \in J \land s \in J)) \to (((x \in X ⟼ A) [r] \subseteq v \land (x \in X ⟼ B) [s] \subseteq w) \to (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq v \times w)$
118	62 117	anim12d	$⊢ ((φ \land (v \in K \land w \in L)) \land (r \in J \land s \in J)) \to (((D \in r \land D \in s) \land ((x \in X ⟼ A) [r] \subseteq v \land (x \in X ⟼ B) [s] \subseteq w)) \to (D \in (r \cap s) \land (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq v \times w))$
119	59 118	biimtrid	$⊢ ((φ \land (v \in K \land w \in L)) \land (r \in J \land s \in J)) \to (((D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land (D \in s \land (x \in X ⟼ B) [s] \subseteq w)) \to (D \in (r \cap s) \land (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq v \times w))$
120		topontop	$⊢ J \in TopOn (X) \to J \in Top$
121	1 120	syl	$⊢ φ \to J \in Top$
122		inopn	$⊢ (J \in Top \land r \in J \land s \in J) \to r \cap s \in J$
123	122	3expb	$⊢ (J \in Top \land (r \in J \land s \in J)) \to r \cap s \in J$
124	121 123	sylan	$⊢ (φ \land (r \in J \land s \in J)) \to r \cap s \in J$
125	124	adantlr	$⊢ ((φ \land (v \in K \land w \in L)) \land (r \in J \land s \in J)) \to r \cap s \in J$
126	119 125	jctild	$⊢ ((φ \land (v \in K \land w \in L)) \land (r \in J \land s \in J)) \to (((D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land (D \in s \land (x \in X ⟼ B) [s] \subseteq w)) \to (r \cap s \in J \land (D \in (r \cap s) \land (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq v \times w)))$
127	126	expimpd	$⊢ (φ \land (v \in K \land w \in L)) \to (((r \in J \land s \in J) \land ((D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land (D \in s \land (x \in X ⟼ B) [s] \subseteq w))) \to (r \cap s \in J \land (D \in (r \cap s) \land (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq v \times w)))$
128		eleq2	$⊢ z = r \cap s \to (D \in z \leftrightarrow D \in (r \cap s))$
129		imaeq2	$⊢ z = r \cap s \to (x \in X ⟼ ⟨A, B⟩) [z] = (x \in X ⟼ ⟨A, B⟩) [r \cap s]$
130	129	sseq1d	$⊢ z = r \cap s \to ((x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w \leftrightarrow (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq v \times w)$
131	128 130	anbi12d	$⊢ z = r \cap s \to ((D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w) \leftrightarrow (D \in (r \cap s) \land (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq v \times w))$
132	131	rspcev	$⊢ (r \cap s \in J \land (D \in (r \cap s) \land (x \in X ⟼ ⟨A, B⟩) [r \cap s] \subseteq v \times w)) \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w)$
133	127 132	syl6	$⊢ (φ \land (v \in K \land w \in L)) \to (((r \in J \land s \in J) \land ((D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land (D \in s \land (x \in X ⟼ B) [s] \subseteq w))) \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w))$
134	133	expd	$⊢ (φ \land (v \in K \land w \in L)) \to ((r \in J \land s \in J) \to (((D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land (D \in s \land (x \in X ⟼ B) [s] \subseteq w)) \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w)))$
135	134	rexlimdvv	$⊢ (φ \land (v \in K \land w \in L)) \to (\exists r \in J \exists s \in J ((D \in r \land (x \in X ⟼ A) [r] \subseteq v) \land (D \in s \land (x \in X ⟼ B) [s] \subseteq w)) \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w))$
136	58 135	syld	$⊢ (φ \land (v \in K \land w \in L)) \to ((x \in X ⟼ ⟨A, B⟩) (D) \in (v \times w) \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w))$
137	136	ralrimivva	$⊢ φ \to \forall v \in K \forall w \in L ((x \in X ⟼ ⟨A, B⟩) (D) \in (v \times w) \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w))$
138		vex	$⊢ v \in V$
139		vex	$⊢ w \in V$
140	138 139	xpex	$⊢ v \times w \in V$
141	140	rgen2w	$⊢ \forall v \in K \forall w \in L v \times w \in V$
142		eqid	$⊢ (v \in K, w \in L ⟼ v \times w) = (v \in K, w \in L ⟼ v \times w)$
143		eleq2	$⊢ y = v \times w \to ((x \in X ⟼ ⟨A, B⟩) (D) \in y \leftrightarrow (x \in X ⟼ ⟨A, B⟩) (D) \in (v \times w))$
144		sseq2	$⊢ y = v \times w \to ((x \in X ⟼ ⟨A, B⟩) [z] \subseteq y \leftrightarrow (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w)$
145	144	anbi2d	$⊢ y = v \times w \to ((D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq y) \leftrightarrow (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w))$
146	145	rexbidv	$⊢ y = v \times w \to (\exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq y) \leftrightarrow \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w))$
147	143 146	imbi12d	$⊢ y = v \times w \to (((x \in X ⟼ ⟨A, B⟩) (D) \in y \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq y)) \leftrightarrow ((x \in X ⟼ ⟨A, B⟩) (D) \in (v \times w) \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w)))$
148	142 147	ralrnmpo	$⊢ \forall v \in K \forall w \in L v \times w \in V \to (\forall y \in ran (v \in K, w \in L ⟼ v \times w) ((x \in X ⟼ ⟨A, B⟩) (D) \in y \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq y)) \leftrightarrow \forall v \in K \forall w \in L ((x \in X ⟼ ⟨A, B⟩) (D) \in (v \times w) \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w)))$
149	141 148	ax-mp	$⊢ \forall y \in ran (v \in K, w \in L ⟼ v \times w) ((x \in X ⟼ ⟨A, B⟩) (D) \in y \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq y)) \leftrightarrow \forall v \in K \forall w \in L ((x \in X ⟼ ⟨A, B⟩) (D) \in (v \times w) \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq v \times w))$
150	137 149	sylibr	$⊢ φ \to \forall y \in ran (v \in K, w \in L ⟼ v \times w) ((x \in X ⟼ ⟨A, B⟩) (D) \in y \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq y))$
151		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
152	2 151	syl	$⊢ φ \to K \in Top$
153		topontop	$⊢ L \in TopOn (Z) \to L \in Top$
154	3 153	syl	$⊢ φ \to L \in Top$
155		eqid	$⊢ ran (v \in K, w \in L ⟼ v \times w) = ran (v \in K, w \in L ⟼ v \times w)$
156	155	txval	$⊢ (K \in Top \land L \in Top) \to K \times_{t} L = topGen (ran (v \in K, w \in L ⟼ v \times w))$
157	152 154 156	syl2anc	$⊢ φ \to K \times_{t} L = topGen (ran (v \in K, w \in L ⟼ v \times w))$
158		txtopon	$⊢ (K \in TopOn (Y) \land L \in TopOn (Z)) \to K \times_{t} L \in TopOn (Y \times Z)$
159	2 3 158	syl2anc	$⊢ φ \to K \times_{t} L \in TopOn (Y \times Z)$
160	1 157 159 4	tgcnp	$⊢ φ \to ((x \in X ⟼ ⟨A, B⟩) \in (J CnP (K \times_{t} L)) (D) \leftrightarrow ((x \in X ⟼ ⟨A, B⟩) : X ⟶ Y \times Z \land \forall y \in ran (v \in K, w \in L ⟼ v \times w) ((x \in X ⟼ ⟨A, B⟩) (D) \in y \to \exists z \in J (D \in z \land (x \in X ⟼ ⟨A, B⟩) [z] \subseteq y))))$
161	14 150 160	mpbir2and	$⊢ φ \to (x \in X ⟼ ⟨A, B⟩) \in (J CnP (K \times_{t} L)) (D)$

Metamath Proof Explorer

Theorem txcnp

Proof