txhmeo

Description: Lift a pair of homeomorphisms on the factors to a homeomorphism of product topologies. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	txhmeo.1	$⊢ X = ⋃ J$
	txhmeo.2	$⊢ Y = ⋃ K$
	txhmeo.3	$⊢ φ \to F \in (J Homeo L)$
	txhmeo.4	$⊢ φ \to G \in (K Homeo M)$
Assertion	txhmeo	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩) \in ((J \times_{t} K) Homeo (L \times_{t} M))$

Proof

Step	Hyp	Ref	Expression
1		txhmeo.1	$⊢ X = ⋃ J$
2		txhmeo.2	$⊢ Y = ⋃ K$
3		txhmeo.3	$⊢ φ \to F \in (J Homeo L)$
4		txhmeo.4	$⊢ φ \to G \in (K Homeo M)$
5		hmeocn	$⊢ F \in (J Homeo L) \to F \in (J Cn L)$
6	3 5	syl	$⊢ φ \to F \in (J Cn L)$
7		cntop1	$⊢ F \in (J Cn L) \to J \in Top$
8	6 7	syl	$⊢ φ \to J \in Top$
9	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
10	8 9	sylib	$⊢ φ \to J \in TopOn (X)$
11		hmeocn	$⊢ G \in (K Homeo M) \to G \in (K Cn M)$
12	4 11	syl	$⊢ φ \to G \in (K Cn M)$
13		cntop1	$⊢ G \in (K Cn M) \to K \in Top$
14	12 13	syl	$⊢ φ \to K \in Top$
15	2	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (Y)$
16	14 15	sylib	$⊢ φ \to K \in TopOn (Y)$
17	10 16	cnmpt1st	$⊢ φ \to (x \in X, y \in Y ⟼ x) \in ((J \times_{t} K) Cn J)$
18	10 16 17 6	cnmpt21f	$⊢ φ \to (x \in X, y \in Y ⟼ F (x)) \in ((J \times_{t} K) Cn L)$
19	10 16	cnmpt2nd	$⊢ φ \to (x \in X, y \in Y ⟼ y) \in ((J \times_{t} K) Cn K)$
20	10 16 19 12	cnmpt21f	$⊢ φ \to (x \in X, y \in Y ⟼ G (y)) \in ((J \times_{t} K) Cn M)$
21	10 16 18 20	cnmpt2t	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩) \in ((J \times_{t} K) Cn (L \times_{t} M))$
22		vex	$⊢ x \in V$
23		vex	$⊢ y \in V$
24	22 23	op1std	$⊢ u = ⟨x, y⟩ \to 1^{st} (u) = x$
25	24	fveq2d	$⊢ u = ⟨x, y⟩ \to F (1^{st} (u)) = F (x)$
26	22 23	op2ndd	$⊢ u = ⟨x, y⟩ \to 2^{nd} (u) = y$
27	26	fveq2d	$⊢ u = ⟨x, y⟩ \to G (2^{nd} (u)) = G (y)$
28	25 27	opeq12d	$⊢ u = ⟨x, y⟩ \to ⟨F (1^{st} (u)), G (2^{nd} (u))⟩ = ⟨F (x), G (y)⟩$
29	28	mpompt	$⊢ (u \in (X \times Y) ⟼ ⟨F (1^{st} (u)), G (2^{nd} (u))⟩) = (x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩)$
30	29	eqcomi	$⊢ (x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩) = (u \in (X \times Y) ⟼ ⟨F (1^{st} (u)), G (2^{nd} (u))⟩)$
31		eqid	$⊢ ⋃ L = ⋃ L$
32	1 31	cnf	$⊢ F \in (J Cn L) \to F : X ⟶ ⋃ L$
33	6 32	syl	$⊢ φ \to F : X ⟶ ⋃ L$
34		xp1st	$⊢ u \in (X \times Y) \to 1^{st} (u) \in X$
35		ffvelcdm	$⊢ (F : X ⟶ ⋃ L \land 1^{st} (u) \in X) \to F (1^{st} (u)) \in ⋃ L$
36	33 34 35	syl2an	$⊢ (φ \land u \in (X \times Y)) \to F (1^{st} (u)) \in ⋃ L$
37		eqid	$⊢ ⋃ M = ⋃ M$
38	2 37	cnf	$⊢ G \in (K Cn M) \to G : Y ⟶ ⋃ M$
39	12 38	syl	$⊢ φ \to G : Y ⟶ ⋃ M$
40		xp2nd	$⊢ u \in (X \times Y) \to 2^{nd} (u) \in Y$
41		ffvelcdm	$⊢ (G : Y ⟶ ⋃ M \land 2^{nd} (u) \in Y) \to G (2^{nd} (u)) \in ⋃ M$
42	39 40 41	syl2an	$⊢ (φ \land u \in (X \times Y)) \to G (2^{nd} (u)) \in ⋃ M$
43	36 42	opelxpd	$⊢ (φ \land u \in (X \times Y)) \to ⟨F (1^{st} (u)), G (2^{nd} (u))⟩ \in (⋃ L \times ⋃ M)$
44	1 31	hmeof1o	$⊢ F \in (J Homeo L) \to F : X \underset{1-1 onto}{⟶} ⋃ L$
45	3 44	syl	$⊢ φ \to F : X \underset{1-1 onto}{⟶} ⋃ L$
46		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} ⋃ L \to F^{-1} : ⋃ L \underset{1-1 onto}{⟶} X$
47		f1of	$⊢ F^{-1} : ⋃ L \underset{1-1 onto}{⟶} X \to F^{-1} : ⋃ L ⟶ X$
48	45 46 47	3syl	$⊢ φ \to F^{-1} : ⋃ L ⟶ X$
49		xp1st	$⊢ v \in (⋃ L \times ⋃ M) \to 1^{st} (v) \in ⋃ L$
50		ffvelcdm	$⊢ (F^{-1} : ⋃ L ⟶ X \land 1^{st} (v) \in ⋃ L) \to F^{-1} (1^{st} (v)) \in X$
51	48 49 50	syl2an	$⊢ (φ \land v \in (⋃ L \times ⋃ M)) \to F^{-1} (1^{st} (v)) \in X$
52	2 37	hmeof1o	$⊢ G \in (K Homeo M) \to G : Y \underset{1-1 onto}{⟶} ⋃ M$
53	4 52	syl	$⊢ φ \to G : Y \underset{1-1 onto}{⟶} ⋃ M$
54		f1ocnv	$⊢ G : Y \underset{1-1 onto}{⟶} ⋃ M \to G^{-1} : ⋃ M \underset{1-1 onto}{⟶} Y$
55		f1of	$⊢ G^{-1} : ⋃ M \underset{1-1 onto}{⟶} Y \to G^{-1} : ⋃ M ⟶ Y$
56	53 54 55	3syl	$⊢ φ \to G^{-1} : ⋃ M ⟶ Y$
57		xp2nd	$⊢ v \in (⋃ L \times ⋃ M) \to 2^{nd} (v) \in ⋃ M$
58		ffvelcdm	$⊢ (G^{-1} : ⋃ M ⟶ Y \land 2^{nd} (v) \in ⋃ M) \to G^{-1} (2^{nd} (v)) \in Y$
59	56 57 58	syl2an	$⊢ (φ \land v \in (⋃ L \times ⋃ M)) \to G^{-1} (2^{nd} (v)) \in Y$
60	51 59	opelxpd	$⊢ (φ \land v \in (⋃ L \times ⋃ M)) \to ⟨F^{-1} (1^{st} (v)), G^{-1} (2^{nd} (v))⟩ \in (X \times Y)$
61	45	adantr	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to F : X \underset{1-1 onto}{⟶} ⋃ L$
62	34	ad2antrl	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to 1^{st} (u) \in X$
63	49	ad2antll	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to 1^{st} (v) \in ⋃ L$
64		f1ocnvfvb	$⊢ (F : X \underset{1-1 onto}{⟶} ⋃ L \land 1^{st} (u) \in X \land 1^{st} (v) \in ⋃ L) \to (F (1^{st} (u)) = 1^{st} (v) \leftrightarrow F^{-1} (1^{st} (v)) = 1^{st} (u))$
65	61 62 63 64	syl3anc	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to (F (1^{st} (u)) = 1^{st} (v) \leftrightarrow F^{-1} (1^{st} (v)) = 1^{st} (u))$
66		eqcom	$⊢ 1^{st} (v) = F (1^{st} (u)) \leftrightarrow F (1^{st} (u)) = 1^{st} (v)$
67		eqcom	$⊢ 1^{st} (u) = F^{-1} (1^{st} (v)) \leftrightarrow F^{-1} (1^{st} (v)) = 1^{st} (u)$
68	65 66 67	3bitr4g	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to (1^{st} (v) = F (1^{st} (u)) \leftrightarrow 1^{st} (u) = F^{-1} (1^{st} (v)))$
69	53	adantr	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to G : Y \underset{1-1 onto}{⟶} ⋃ M$
70	40	ad2antrl	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to 2^{nd} (u) \in Y$
71	57	ad2antll	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to 2^{nd} (v) \in ⋃ M$
72		f1ocnvfvb	$⊢ (G : Y \underset{1-1 onto}{⟶} ⋃ M \land 2^{nd} (u) \in Y \land 2^{nd} (v) \in ⋃ M) \to (G (2^{nd} (u)) = 2^{nd} (v) \leftrightarrow G^{-1} (2^{nd} (v)) = 2^{nd} (u))$
73	69 70 71 72	syl3anc	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to (G (2^{nd} (u)) = 2^{nd} (v) \leftrightarrow G^{-1} (2^{nd} (v)) = 2^{nd} (u))$
74		eqcom	$⊢ 2^{nd} (v) = G (2^{nd} (u)) \leftrightarrow G (2^{nd} (u)) = 2^{nd} (v)$
75		eqcom	$⊢ 2^{nd} (u) = G^{-1} (2^{nd} (v)) \leftrightarrow G^{-1} (2^{nd} (v)) = 2^{nd} (u)$
76	73 74 75	3bitr4g	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to (2^{nd} (v) = G (2^{nd} (u)) \leftrightarrow 2^{nd} (u) = G^{-1} (2^{nd} (v)))$
77	68 76	anbi12d	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to ((1^{st} (v) = F (1^{st} (u)) \land 2^{nd} (v) = G (2^{nd} (u))) \leftrightarrow (1^{st} (u) = F^{-1} (1^{st} (v)) \land 2^{nd} (u) = G^{-1} (2^{nd} (v))))$
78		eqop	$⊢ v \in (⋃ L \times ⋃ M) \to (v = ⟨F (1^{st} (u)), G (2^{nd} (u))⟩ \leftrightarrow (1^{st} (v) = F (1^{st} (u)) \land 2^{nd} (v) = G (2^{nd} (u))))$
79	78	ad2antll	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to (v = ⟨F (1^{st} (u)), G (2^{nd} (u))⟩ \leftrightarrow (1^{st} (v) = F (1^{st} (u)) \land 2^{nd} (v) = G (2^{nd} (u))))$
80		eqop	$⊢ u \in (X \times Y) \to (u = ⟨F^{-1} (1^{st} (v)), G^{-1} (2^{nd} (v))⟩ \leftrightarrow (1^{st} (u) = F^{-1} (1^{st} (v)) \land 2^{nd} (u) = G^{-1} (2^{nd} (v))))$
81	80	ad2antrl	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to (u = ⟨F^{-1} (1^{st} (v)), G^{-1} (2^{nd} (v))⟩ \leftrightarrow (1^{st} (u) = F^{-1} (1^{st} (v)) \land 2^{nd} (u) = G^{-1} (2^{nd} (v))))$
82	77 79 81	3bitr4rd	$⊢ (φ \land (u \in (X \times Y) \land v \in (⋃ L \times ⋃ M))) \to (u = ⟨F^{-1} (1^{st} (v)), G^{-1} (2^{nd} (v))⟩ \leftrightarrow v = ⟨F (1^{st} (u)), G (2^{nd} (u))⟩)$
83	30 43 60 82	f1ocnv2d	$⊢ φ \to ((x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩) : X \times Y \underset{1-1 onto}{⟶} ⋃ L \times ⋃ M \land {(x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩)}^{-1} = (v \in (⋃ L \times ⋃ M) ⟼ ⟨F^{-1} (1^{st} (v)), G^{-1} (2^{nd} (v))⟩))$
84	83	simprd	$⊢ φ \to {(x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩)}^{-1} = (v \in (⋃ L \times ⋃ M) ⟼ ⟨F^{-1} (1^{st} (v)), G^{-1} (2^{nd} (v))⟩)$
85		vex	$⊢ z \in V$
86		vex	$⊢ w \in V$
87	85 86	op1std	$⊢ v = ⟨z, w⟩ \to 1^{st} (v) = z$
88	87	fveq2d	$⊢ v = ⟨z, w⟩ \to F^{-1} (1^{st} (v)) = F^{-1} (z)$
89	85 86	op2ndd	$⊢ v = ⟨z, w⟩ \to 2^{nd} (v) = w$
90	89	fveq2d	$⊢ v = ⟨z, w⟩ \to G^{-1} (2^{nd} (v)) = G^{-1} (w)$
91	88 90	opeq12d	$⊢ v = ⟨z, w⟩ \to ⟨F^{-1} (1^{st} (v)), G^{-1} (2^{nd} (v))⟩ = ⟨F^{-1} (z), G^{-1} (w)⟩$
92	91	mpompt	$⊢ (v \in (⋃ L \times ⋃ M) ⟼ ⟨F^{-1} (1^{st} (v)), G^{-1} (2^{nd} (v))⟩) = (z \in ⋃ L, w \in ⋃ M ⟼ ⟨F^{-1} (z), G^{-1} (w)⟩)$
93	84 92	eqtrdi	$⊢ φ \to {(x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩)}^{-1} = (z \in ⋃ L, w \in ⋃ M ⟼ ⟨F^{-1} (z), G^{-1} (w)⟩)$
94		cntop2	$⊢ F \in (J Cn L) \to L \in Top$
95	6 94	syl	$⊢ φ \to L \in Top$
96	31	toptopon	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
97	95 96	sylib	$⊢ φ \to L \in TopOn (⋃ L)$
98		cntop2	$⊢ G \in (K Cn M) \to M \in Top$
99	12 98	syl	$⊢ φ \to M \in Top$
100	37	toptopon	$⊢ M \in Top \leftrightarrow M \in TopOn (⋃ M)$
101	99 100	sylib	$⊢ φ \to M \in TopOn (⋃ M)$
102	97 101	cnmpt1st	$⊢ φ \to (z \in ⋃ L, w \in ⋃ M ⟼ z) \in ((L \times_{t} M) Cn L)$
103		hmeocnvcn	$⊢ F \in (J Homeo L) \to F^{-1} \in (L Cn J)$
104	3 103	syl	$⊢ φ \to F^{-1} \in (L Cn J)$
105	97 101 102 104	cnmpt21f	$⊢ φ \to (z \in ⋃ L, w \in ⋃ M ⟼ F^{-1} (z)) \in ((L \times_{t} M) Cn J)$
106	97 101	cnmpt2nd	$⊢ φ \to (z \in ⋃ L, w \in ⋃ M ⟼ w) \in ((L \times_{t} M) Cn M)$
107		hmeocnvcn	$⊢ G \in (K Homeo M) \to G^{-1} \in (M Cn K)$
108	4 107	syl	$⊢ φ \to G^{-1} \in (M Cn K)$
109	97 101 106 108	cnmpt21f	$⊢ φ \to (z \in ⋃ L, w \in ⋃ M ⟼ G^{-1} (w)) \in ((L \times_{t} M) Cn K)$
110	97 101 105 109	cnmpt2t	$⊢ φ \to (z \in ⋃ L, w \in ⋃ M ⟼ ⟨F^{-1} (z), G^{-1} (w)⟩) \in ((L \times_{t} M) Cn (J \times_{t} K))$
111	93 110	eqeltrd	$⊢ φ \to {(x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩)}^{-1} \in ((L \times_{t} M) Cn (J \times_{t} K))$
112		ishmeo	$⊢ (x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩) \in ((J \times_{t} K) Homeo (L \times_{t} M)) \leftrightarrow ((x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩) \in ((J \times_{t} K) Cn (L \times_{t} M)) \land {(x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩)}^{-1} \in ((L \times_{t} M) Cn (J \times_{t} K)))$
113	21 111 112	sylanbrc	$⊢ φ \to (x \in X, y \in Y ⟼ ⟨F (x), G (y)⟩) \in ((J \times_{t} K) Homeo (L \times_{t} M))$

Metamath Proof Explorer

Theorem txhmeo

Proof