txomap

Description: Given two open maps F and G , H mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019)

	Ref	Expression
Hypotheses	txomap.f	$⊢ φ \to F : X ⟶ Z$
	txomap.g	$⊢ φ \to G : Y ⟶ T$
	txomap.j	$⊢ φ \to J \in TopOn (X)$
	txomap.k	$⊢ φ \to K \in TopOn (Y)$
	txomap.l	$⊢ φ \to L \in TopOn (Z)$
	txomap.m	$⊢ φ \to M \in TopOn (T)$
	txomap.1	$⊢ (φ \land x \in J) \to F [x] \in L$
	txomap.2	$⊢ (φ \land y \in K) \to G [y] \in M$
	txomap.a	$⊢ φ \to A \in (J \times_{t} K)$
	txomap.h	$⊢ H = (x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩)$
Assertion	txomap	$⊢ φ \to H [A] \in (L \times_{t} M)$

Proof

Step	Hyp	Ref	Expression
1		txomap.f	$⊢ φ \to F : X ⟶ Z$
2		txomap.g	$⊢ φ \to G : Y ⟶ T$
3		txomap.j	$⊢ φ \to J \in TopOn (X)$
4		txomap.k	$⊢ φ \to K \in TopOn (Y)$
5		txomap.l	$⊢ φ \to L \in TopOn (Z)$
6		txomap.m	$⊢ φ \to M \in TopOn (T)$
7		txomap.1	$⊢ (φ \land x \in J) \to F [x] \in L$
8		txomap.2	$⊢ (φ \land y \in K) \to G [y] \in M$
9		txomap.a	$⊢ φ \to A \in (J \times_{t} K)$
10		txomap.h	$⊢ H = (x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩)$
11		simp-6l	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to φ$
12		simpllr	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to x \in J$
13	11 12 7	syl2anc	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to F [x] \in L$
14		simplr	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to y \in K$
15	11 14 8	syl2anc	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to G [y] \in M$
16		opex	$⊢ ⟨F (x), G (y)⟩ \in V$
17	10 16	fnmpoi	$⊢ H Fn (X \times Y)$
18	3	ad6antr	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to J \in TopOn (X)$
19		toponss	$⊢ (J \in TopOn (X) \land x \in J) \to x \subseteq X$
20	18 12 19	syl2anc	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to x \subseteq X$
21	4	ad6antr	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to K \in TopOn (Y)$
22		toponss	$⊢ (K \in TopOn (Y) \land y \in K) \to y \subseteq Y$
23	21 14 22	syl2anc	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to y \subseteq Y$
24		xpss12	$⊢ (x \subseteq X \land y \subseteq Y) \to x \times y \subseteq X \times Y$
25	20 23 24	syl2anc	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to x \times y \subseteq X \times Y$
26		simprl	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to z \in (x \times y)$
27		fnfvima	$⊢ (H Fn (X \times Y) \land x \times y \subseteq X \times Y \land z \in (x \times y)) \to H (z) \in H [x \times y]$
28	17 25 26 27	mp3an2i	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to H (z) \in H [x \times y]$
29		simp-4r	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to H (z) = c$
30		ffn	$⊢ F : X ⟶ Z \to F Fn X$
31	11 1 30	3syl	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to F Fn X$
32		ffn	$⊢ G : Y ⟶ T \to G Fn Y$
33	11 2 32	3syl	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to G Fn Y$
34	10 31 33 20 23	fimaproj	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to H [x \times y] = F [x] \times G [y]$
35	28 29 34	3eltr3d	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to c \in (F [x] \times G [y])$
36		imass2	$⊢ x \times y \subseteq A \to H [x \times y] \subseteq H [A]$
37	36	ad2antll	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to H [x \times y] \subseteq H [A]$
38	34 37	eqsstrrd	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to F [x] \times G [y] \subseteq H [A]$
39		xpeq1	$⊢ a = F [x] \to a \times b = F [x] \times b$
40	39	eleq2d	$⊢ a = F [x] \to (c \in (a \times b) \leftrightarrow c \in (F [x] \times b))$
41	39	sseq1d	$⊢ a = F [x] \to (a \times b \subseteq H [A] \leftrightarrow F [x] \times b \subseteq H [A])$
42	40 41	anbi12d	$⊢ a = F [x] \to ((c \in (a \times b) \land a \times b \subseteq H [A]) \leftrightarrow (c \in (F [x] \times b) \land F [x] \times b \subseteq H [A]))$
43		xpeq2	$⊢ b = G [y] \to F [x] \times b = F [x] \times G [y]$
44	43	eleq2d	$⊢ b = G [y] \to (c \in (F [x] \times b) \leftrightarrow c \in (F [x] \times G [y]))$
45	43	sseq1d	$⊢ b = G [y] \to (F [x] \times b \subseteq H [A] \leftrightarrow F [x] \times G [y] \subseteq H [A])$
46	44 45	anbi12d	$⊢ b = G [y] \to ((c \in (F [x] \times b) \land F [x] \times b \subseteq H [A]) \leftrightarrow (c \in (F [x] \times G [y]) \land F [x] \times G [y] \subseteq H [A]))$
47	42 46	rspc2ev	$⊢ (F [x] \in L \land G [y] \in M \land (c \in (F [x] \times G [y]) \land F [x] \times G [y] \subseteq H [A])) \to \exists a \in L \exists b \in M (c \in (a \times b) \land a \times b \subseteq H [A])$
48	13 15 35 38 47	syl112anc	$⊢ ((((((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \land x \in J) \land y \in K) \land (z \in (x \times y) \land x \times y \subseteq A)) \to \exists a \in L \exists b \in M (c \in (a \times b) \land a \times b \subseteq H [A])$
49		eltx	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to (A \in (J \times_{t} K) \leftrightarrow \forall z \in A \exists x \in J \exists y \in K (z \in (x \times y) \land x \times y \subseteq A))$
50	3 4 49	syl2anc	$⊢ φ \to (A \in (J \times_{t} K) \leftrightarrow \forall z \in A \exists x \in J \exists y \in K (z \in (x \times y) \land x \times y \subseteq A))$
51	9 50	mpbid	$⊢ φ \to \forall z \in A \exists x \in J \exists y \in K (z \in (x \times y) \land x \times y \subseteq A)$
52	51	r19.21bi	$⊢ (φ \land z \in A) \to \exists x \in J \exists y \in K (z \in (x \times y) \land x \times y \subseteq A)$
53	52	ad4ant13	$⊢ (((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \to \exists x \in J \exists y \in K (z \in (x \times y) \land x \times y \subseteq A)$
54	48 53	r19.29vva	$⊢ (((φ \land c \in H [A]) \land z \in A) \land H (z) = c) \to \exists a \in L \exists b \in M (c \in (a \times b) \land a \times b \subseteq H [A])$
55	10	mpofun	$⊢ Fun H$
56		fvelima	$⊢ (Fun H \land c \in H [A]) \to \exists z \in A H (z) = c$
57	55 56	mpan	$⊢ c \in H [A] \to \exists z \in A H (z) = c$
58	57	adantl	$⊢ (φ \land c \in H [A]) \to \exists z \in A H (z) = c$
59	54 58	r19.29a	$⊢ (φ \land c \in H [A]) \to \exists a \in L \exists b \in M (c \in (a \times b) \land a \times b \subseteq H [A])$
60	59	ralrimiva	$⊢ φ \to \forall c \in H [A] \exists a \in L \exists b \in M (c \in (a \times b) \land a \times b \subseteq H [A])$
61		eltx	$⊢ (L \in TopOn (Z) \land M \in TopOn (T)) \to (H [A] \in (L \times_{t} M) \leftrightarrow \forall c \in H [A] \exists a \in L \exists b \in M (c \in (a \times b) \land a \times b \subseteq H [A]))$
62	5 6 61	syl2anc	$⊢ φ \to (H [A] \in (L \times_{t} M) \leftrightarrow \forall c \in H [A] \exists a \in L \exists b \in M (c \in (a \times b) \land a \times b \subseteq H [A]))$
63	60 62	mpbird	$⊢ φ \to H [A] \in (L \times_{t} M)$

Metamath Proof Explorer

Theorem txomap

Proof