ptunhmeo

Description: Define a homeomorphism from a binary product of indexed product topologies to an indexed product topology on the union of the index sets. This is the topological analogue of ( A ^ B ) x. ( A ^ C ) = A ^ ( B + C ) . (Contributed by Mario Carneiro, 8-Feb-2015) (Proof shortened by Mario Carneiro, 23-Aug-2015)

	Ref	Expression
Hypotheses	ptunhmeo.x	$⊢ X = ⋃ K$
	ptunhmeo.y	$⊢ Y = ⋃ L$
	ptunhmeo.j	$⊢ J = \prod_{𝑡} (F)$
	ptunhmeo.k	$⊢ K = \prod_{𝑡} ({F ↾}_{A})$
	ptunhmeo.l	$⊢ L = \prod_{𝑡} ({F ↾}_{B})$
	ptunhmeo.g	$⊢ G = (x \in X, y \in Y ⟼ x \cup y)$
	ptunhmeo.c	$⊢ φ \to C \in V$
	ptunhmeo.f	$⊢ φ \to F : C ⟶ Top$
	ptunhmeo.u	$⊢ φ \to C = A \cup B$
	ptunhmeo.i	$⊢ φ \to A \cap B = \emptyset$
Assertion	ptunhmeo	$⊢ φ \to G \in ((K \times_{t} L) Homeo J)$

Proof

Step	Hyp	Ref	Expression
1		ptunhmeo.x	$⊢ X = ⋃ K$
2		ptunhmeo.y	$⊢ Y = ⋃ L$
3		ptunhmeo.j	$⊢ J = \prod_{𝑡} (F)$
4		ptunhmeo.k	$⊢ K = \prod_{𝑡} ({F ↾}_{A})$
5		ptunhmeo.l	$⊢ L = \prod_{𝑡} ({F ↾}_{B})$
6		ptunhmeo.g	$⊢ G = (x \in X, y \in Y ⟼ x \cup y)$
7		ptunhmeo.c	$⊢ φ \to C \in V$
8		ptunhmeo.f	$⊢ φ \to F : C ⟶ Top$
9		ptunhmeo.u	$⊢ φ \to C = A \cup B$
10		ptunhmeo.i	$⊢ φ \to A \cap B = \emptyset$
11		vex	$⊢ x \in V$
12		vex	$⊢ y \in V$
13	11 12	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
14	11 12	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
15	13 14	uneq12d	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) \cup 2^{nd} (z) = x \cup y$
16	15	mpompt	$⊢ (z \in (X \times Y) ⟼ 1^{st} (z) \cup 2^{nd} (z)) = (x \in X, y \in Y ⟼ x \cup y)$
17	6 16	eqtr4i	$⊢ G = (z \in (X \times Y) ⟼ 1^{st} (z) \cup 2^{nd} (z))$
18		xp1st	$⊢ z \in (X \times Y) \to 1^{st} (z) \in X$
19	18	adantl	$⊢ (φ \land z \in (X \times Y)) \to 1^{st} (z) \in X$
20		ixpeq2	$⊢ \forall n \in A ⋃ ({F ↾}_{A}) (n) = ⋃ F (n) \to \underset{n \in A}{⨉} ⋃ ({F ↾}_{A}) (n) = \underset{n \in A}{⨉} ⋃ F (n)$
21		fvres	$⊢ n \in A \to ({F ↾}_{A}) (n) = F (n)$
22	21	unieqd	$⊢ n \in A \to ⋃ ({F ↾}_{A}) (n) = ⋃ F (n)$
23	20 22	mprg	$⊢ \underset{n \in A}{⨉} ⋃ ({F ↾}_{A}) (n) = \underset{n \in A}{⨉} ⋃ F (n)$
24		ssun1	$⊢ A \subseteq A \cup B$
25	24 9	sseqtrrid	$⊢ φ \to A \subseteq C$
26	7 25	ssexd	$⊢ φ \to A \in V$
27	8 25	fssresd	$⊢ φ \to ({F ↾}_{A}) : A ⟶ Top$
28	4	ptuni	$⊢ (A \in V \land ({F ↾}_{A}) : A ⟶ Top) \to \underset{n \in A}{⨉} ⋃ ({F ↾}_{A}) (n) = ⋃ K$
29	26 27 28	syl2anc	$⊢ φ \to \underset{n \in A}{⨉} ⋃ ({F ↾}_{A}) (n) = ⋃ K$
30	23 29	eqtr3id	$⊢ φ \to \underset{n \in A}{⨉} ⋃ F (n) = ⋃ K$
31	30 1	eqtr4di	$⊢ φ \to \underset{n \in A}{⨉} ⋃ F (n) = X$
32	31	adantr	$⊢ (φ \land z \in (X \times Y)) \to \underset{n \in A}{⨉} ⋃ F (n) = X$
33	19 32	eleqtrrd	$⊢ (φ \land z \in (X \times Y)) \to 1^{st} (z) \in \underset{n \in A}{⨉} ⋃ F (n)$
34		xp2nd	$⊢ z \in (X \times Y) \to 2^{nd} (z) \in Y$
35	34	adantl	$⊢ (φ \land z \in (X \times Y)) \to 2^{nd} (z) \in Y$
36	9	eqcomd	$⊢ φ \to A \cup B = C$
37		uneqdifeq	$⊢ (A \subseteq C \land A \cap B = \emptyset) \to (A \cup B = C \leftrightarrow C ∖ A = B)$
38	25 10 37	syl2anc	$⊢ φ \to (A \cup B = C \leftrightarrow C ∖ A = B)$
39	36 38	mpbid	$⊢ φ \to C ∖ A = B$
40	39	ixpeq1d	$⊢ φ \to \underset{n \in C ∖ A}{⨉} ⋃ F (n) = \underset{n \in B}{⨉} ⋃ F (n)$
41		ixpeq2	$⊢ \forall n \in B ⋃ ({F ↾}_{B}) (n) = ⋃ F (n) \to \underset{n \in B}{⨉} ⋃ ({F ↾}_{B}) (n) = \underset{n \in B}{⨉} ⋃ F (n)$
42		fvres	$⊢ n \in B \to ({F ↾}_{B}) (n) = F (n)$
43	42	unieqd	$⊢ n \in B \to ⋃ ({F ↾}_{B}) (n) = ⋃ F (n)$
44	41 43	mprg	$⊢ \underset{n \in B}{⨉} ⋃ ({F ↾}_{B}) (n) = \underset{n \in B}{⨉} ⋃ F (n)$
45		ssun2	$⊢ B \subseteq A \cup B$
46	45 9	sseqtrrid	$⊢ φ \to B \subseteq C$
47	7 46	ssexd	$⊢ φ \to B \in V$
48	8 46	fssresd	$⊢ φ \to ({F ↾}_{B}) : B ⟶ Top$
49	5	ptuni	$⊢ (B \in V \land ({F ↾}_{B}) : B ⟶ Top) \to \underset{n \in B}{⨉} ⋃ ({F ↾}_{B}) (n) = ⋃ L$
50	47 48 49	syl2anc	$⊢ φ \to \underset{n \in B}{⨉} ⋃ ({F ↾}_{B}) (n) = ⋃ L$
51	44 50	eqtr3id	$⊢ φ \to \underset{n \in B}{⨉} ⋃ F (n) = ⋃ L$
52	51 2	eqtr4di	$⊢ φ \to \underset{n \in B}{⨉} ⋃ F (n) = Y$
53	40 52	eqtrd	$⊢ φ \to \underset{n \in C ∖ A}{⨉} ⋃ F (n) = Y$
54	53	adantr	$⊢ (φ \land z \in (X \times Y)) \to \underset{n \in C ∖ A}{⨉} ⋃ F (n) = Y$
55	35 54	eleqtrrd	$⊢ (φ \land z \in (X \times Y)) \to 2^{nd} (z) \in \underset{n \in C ∖ A}{⨉} ⋃ F (n)$
56	25	adantr	$⊢ (φ \land z \in (X \times Y)) \to A \subseteq C$
57		undifixp	$⊢ (1^{st} (z) \in \underset{n \in A}{⨉} ⋃ F (n) \land 2^{nd} (z) \in \underset{n \in C ∖ A}{⨉} ⋃ F (n) \land A \subseteq C) \to 1^{st} (z) \cup 2^{nd} (z) \in \underset{n \in C}{⨉} ⋃ F (n)$
58	33 55 56 57	syl3anc	$⊢ (φ \land z \in (X \times Y)) \to 1^{st} (z) \cup 2^{nd} (z) \in \underset{n \in C}{⨉} ⋃ F (n)$
59		ixpfn	$⊢ 1^{st} (z) \cup 2^{nd} (z) \in \underset{n \in C}{⨉} ⋃ F (n) \to (1^{st} (z) \cup 2^{nd} (z)) Fn C$
60	58 59	syl	$⊢ (φ \land z \in (X \times Y)) \to (1^{st} (z) \cup 2^{nd} (z)) Fn C$
61		dffn5	$⊢ (1^{st} (z) \cup 2^{nd} (z)) Fn C \leftrightarrow 1^{st} (z) \cup 2^{nd} (z) = (k \in C ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k))$
62	60 61	sylib	$⊢ (φ \land z \in (X \times Y)) \to 1^{st} (z) \cup 2^{nd} (z) = (k \in C ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k))$
63	62	mpteq2dva	$⊢ φ \to (z \in (X \times Y) ⟼ 1^{st} (z) \cup 2^{nd} (z)) = (z \in (X \times Y) ⟼ (k \in C ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k)))$
64	17 63	syl5eq	$⊢ φ \to G = (z \in (X \times Y) ⟼ (k \in C ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k)))$
65		pttop	$⊢ (A \in V \land ({F ↾}_{A}) : A ⟶ Top) \to \prod_{𝑡} ({F ↾}_{A}) \in Top$
66	26 27 65	syl2anc	$⊢ φ \to \prod_{𝑡} ({F ↾}_{A}) \in Top$
67	4 66	eqeltrid	$⊢ φ \to K \in Top$
68	1	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (X)$
69	67 68	sylib	$⊢ φ \to K \in TopOn (X)$
70		pttop	$⊢ (B \in V \land ({F ↾}_{B}) : B ⟶ Top) \to \prod_{𝑡} ({F ↾}_{B}) \in Top$
71	47 48 70	syl2anc	$⊢ φ \to \prod_{𝑡} ({F ↾}_{B}) \in Top$
72	5 71	eqeltrid	$⊢ φ \to L \in Top$
73	2	toptopon	$⊢ L \in Top \leftrightarrow L \in TopOn (Y)$
74	72 73	sylib	$⊢ φ \to L \in TopOn (Y)$
75		txtopon	$⊢ (K \in TopOn (X) \land L \in TopOn (Y)) \to K \times_{t} L \in TopOn (X \times Y)$
76	69 74 75	syl2anc	$⊢ φ \to K \times_{t} L \in TopOn (X \times Y)$
77	9	eleq2d	$⊢ φ \to (k \in C \leftrightarrow k \in (A \cup B))$
78	77	biimpa	$⊢ (φ \land k \in C) \to k \in (A \cup B)$
79		elun	$⊢ k \in (A \cup B) \leftrightarrow (k \in A \lor k \in B)$
80	78 79	sylib	$⊢ (φ \land k \in C) \to (k \in A \lor k \in B)$
81		ixpfn	$⊢ 1^{st} (z) \in \underset{n \in A}{⨉} ⋃ F (n) \to 1^{st} (z) Fn A$
82	33 81	syl	$⊢ (φ \land z \in (X \times Y)) \to 1^{st} (z) Fn A$
83	82	adantlr	$⊢ ((φ \land k \in A) \land z \in (X \times Y)) \to 1^{st} (z) Fn A$
84	52	adantr	$⊢ (φ \land z \in (X \times Y)) \to \underset{n \in B}{⨉} ⋃ F (n) = Y$
85	35 84	eleqtrrd	$⊢ (φ \land z \in (X \times Y)) \to 2^{nd} (z) \in \underset{n \in B}{⨉} ⋃ F (n)$
86		ixpfn	$⊢ 2^{nd} (z) \in \underset{n \in B}{⨉} ⋃ F (n) \to 2^{nd} (z) Fn B$
87	85 86	syl	$⊢ (φ \land z \in (X \times Y)) \to 2^{nd} (z) Fn B$
88	87	adantlr	$⊢ ((φ \land k \in A) \land z \in (X \times Y)) \to 2^{nd} (z) Fn B$
89	10	ad2antrr	$⊢ ((φ \land k \in A) \land z \in (X \times Y)) \to A \cap B = \emptyset$
90		simplr	$⊢ ((φ \land k \in A) \land z \in (X \times Y)) \to k \in A$
91		fvun1	$⊢ (1^{st} (z) Fn A \land 2^{nd} (z) Fn B \land (A \cap B = \emptyset \land k \in A)) \to (1^{st} (z) \cup 2^{nd} (z)) (k) = 1^{st} (z) (k)$
92	83 88 89 90 91	syl112anc	$⊢ ((φ \land k \in A) \land z \in (X \times Y)) \to (1^{st} (z) \cup 2^{nd} (z)) (k) = 1^{st} (z) (k)$
93	92	mpteq2dva	$⊢ (φ \land k \in A) \to (z \in (X \times Y) ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k)) = (z \in (X \times Y) ⟼ 1^{st} (z) (k))$
94	76	adantr	$⊢ (φ \land k \in A) \to K \times_{t} L \in TopOn (X \times Y)$
95	13	mpompt	$⊢ (z \in (X \times Y) ⟼ 1^{st} (z)) = (x \in X, y \in Y ⟼ x)$
96	69	adantr	$⊢ (φ \land k \in A) \to K \in TopOn (X)$
97	74	adantr	$⊢ (φ \land k \in A) \to L \in TopOn (Y)$
98	96 97	cnmpt1st	$⊢ (φ \land k \in A) \to (x \in X, y \in Y ⟼ x) \in ((K \times_{t} L) Cn K)$
99	95 98	eqeltrid	$⊢ (φ \land k \in A) \to (z \in (X \times Y) ⟼ 1^{st} (z)) \in ((K \times_{t} L) Cn K)$
100	26	adantr	$⊢ (φ \land k \in A) \to A \in V$
101	27	adantr	$⊢ (φ \land k \in A) \to ({F ↾}_{A}) : A ⟶ Top$
102		simpr	$⊢ (φ \land k \in A) \to k \in A$
103	1 4	ptpjcn	$⊢ (A \in V \land ({F ↾}_{A}) : A ⟶ Top \land k \in A) \to (f \in X ⟼ f (k)) \in (K Cn ({F ↾}_{A}) (k))$
104	100 101 102 103	syl3anc	$⊢ (φ \land k \in A) \to (f \in X ⟼ f (k)) \in (K Cn ({F ↾}_{A}) (k))$
105		fvres	$⊢ k \in A \to ({F ↾}_{A}) (k) = F (k)$
106	105	adantl	$⊢ (φ \land k \in A) \to ({F ↾}_{A}) (k) = F (k)$
107	106	oveq2d	$⊢ (φ \land k \in A) \to K Cn ({F ↾}_{A}) (k) = K Cn F (k)$
108	104 107	eleqtrd	$⊢ (φ \land k \in A) \to (f \in X ⟼ f (k)) \in (K Cn F (k))$
109		fveq1	$⊢ f = 1^{st} (z) \to f (k) = 1^{st} (z) (k)$
110	94 99 96 108 109	cnmpt11	$⊢ (φ \land k \in A) \to (z \in (X \times Y) ⟼ 1^{st} (z) (k)) \in ((K \times_{t} L) Cn F (k))$
111	93 110	eqeltrd	$⊢ (φ \land k \in A) \to (z \in (X \times Y) ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k)) \in ((K \times_{t} L) Cn F (k))$
112	82	adantlr	$⊢ ((φ \land k \in B) \land z \in (X \times Y)) \to 1^{st} (z) Fn A$
113	87	adantlr	$⊢ ((φ \land k \in B) \land z \in (X \times Y)) \to 2^{nd} (z) Fn B$
114	10	ad2antrr	$⊢ ((φ \land k \in B) \land z \in (X \times Y)) \to A \cap B = \emptyset$
115		simplr	$⊢ ((φ \land k \in B) \land z \in (X \times Y)) \to k \in B$
116		fvun2	$⊢ (1^{st} (z) Fn A \land 2^{nd} (z) Fn B \land (A \cap B = \emptyset \land k \in B)) \to (1^{st} (z) \cup 2^{nd} (z)) (k) = 2^{nd} (z) (k)$
117	112 113 114 115 116	syl112anc	$⊢ ((φ \land k \in B) \land z \in (X \times Y)) \to (1^{st} (z) \cup 2^{nd} (z)) (k) = 2^{nd} (z) (k)$
118	117	mpteq2dva	$⊢ (φ \land k \in B) \to (z \in (X \times Y) ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k)) = (z \in (X \times Y) ⟼ 2^{nd} (z) (k))$
119	76	adantr	$⊢ (φ \land k \in B) \to K \times_{t} L \in TopOn (X \times Y)$
120	14	mpompt	$⊢ (z \in (X \times Y) ⟼ 2^{nd} (z)) = (x \in X, y \in Y ⟼ y)$
121	69	adantr	$⊢ (φ \land k \in B) \to K \in TopOn (X)$
122	74	adantr	$⊢ (φ \land k \in B) \to L \in TopOn (Y)$
123	121 122	cnmpt2nd	$⊢ (φ \land k \in B) \to (x \in X, y \in Y ⟼ y) \in ((K \times_{t} L) Cn L)$
124	120 123	eqeltrid	$⊢ (φ \land k \in B) \to (z \in (X \times Y) ⟼ 2^{nd} (z)) \in ((K \times_{t} L) Cn L)$
125	47	adantr	$⊢ (φ \land k \in B) \to B \in V$
126	48	adantr	$⊢ (φ \land k \in B) \to ({F ↾}_{B}) : B ⟶ Top$
127		simpr	$⊢ (φ \land k \in B) \to k \in B$
128	2 5	ptpjcn	$⊢ (B \in V \land ({F ↾}_{B}) : B ⟶ Top \land k \in B) \to (f \in Y ⟼ f (k)) \in (L Cn ({F ↾}_{B}) (k))$
129	125 126 127 128	syl3anc	$⊢ (φ \land k \in B) \to (f \in Y ⟼ f (k)) \in (L Cn ({F ↾}_{B}) (k))$
130		fvres	$⊢ k \in B \to ({F ↾}_{B}) (k) = F (k)$
131	130	adantl	$⊢ (φ \land k \in B) \to ({F ↾}_{B}) (k) = F (k)$
132	131	oveq2d	$⊢ (φ \land k \in B) \to L Cn ({F ↾}_{B}) (k) = L Cn F (k)$
133	129 132	eleqtrd	$⊢ (φ \land k \in B) \to (f \in Y ⟼ f (k)) \in (L Cn F (k))$
134		fveq1	$⊢ f = 2^{nd} (z) \to f (k) = 2^{nd} (z) (k)$
135	119 124 122 133 134	cnmpt11	$⊢ (φ \land k \in B) \to (z \in (X \times Y) ⟼ 2^{nd} (z) (k)) \in ((K \times_{t} L) Cn F (k))$
136	118 135	eqeltrd	$⊢ (φ \land k \in B) \to (z \in (X \times Y) ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k)) \in ((K \times_{t} L) Cn F (k))$
137	111 136	jaodan	$⊢ (φ \land (k \in A \lor k \in B)) \to (z \in (X \times Y) ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k)) \in ((K \times_{t} L) Cn F (k))$
138	80 137	syldan	$⊢ (φ \land k \in C) \to (z \in (X \times Y) ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k)) \in ((K \times_{t} L) Cn F (k))$
139	3 76 7 8 138	ptcn	$⊢ φ \to (z \in (X \times Y) ⟼ (k \in C ⟼ (1^{st} (z) \cup 2^{nd} (z)) (k))) \in ((K \times_{t} L) Cn J)$
140	64 139	eqeltrd	$⊢ φ \to G \in ((K \times_{t} L) Cn J)$
141	1 2 3 4 5 6 7 8 9 10	ptuncnv	$⊢ φ \to G^{-1} = (z \in ⋃ J ⟼ ⟨{z ↾}_{A}, {z ↾}_{B}⟩)$
142		pttop	$⊢ (C \in V \land F : C ⟶ Top) \to \prod_{𝑡} (F) \in Top$
143	7 8 142	syl2anc	$⊢ φ \to \prod_{𝑡} (F) \in Top$
144	3 143	eqeltrid	$⊢ φ \to J \in Top$
145		eqid	$⊢ ⋃ J = ⋃ J$
146	145	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
147	144 146	sylib	$⊢ φ \to J \in TopOn (⋃ J)$
148	145 3 4	ptrescn	$⊢ (C \in V \land F : C ⟶ Top \land A \subseteq C) \to (z \in ⋃ J ⟼ {z ↾}_{A}) \in (J Cn K)$
149	7 8 25 148	syl3anc	$⊢ φ \to (z \in ⋃ J ⟼ {z ↾}_{A}) \in (J Cn K)$
150	145 3 5	ptrescn	$⊢ (C \in V \land F : C ⟶ Top \land B \subseteq C) \to (z \in ⋃ J ⟼ {z ↾}_{B}) \in (J Cn L)$
151	7 8 46 150	syl3anc	$⊢ φ \to (z \in ⋃ J ⟼ {z ↾}_{B}) \in (J Cn L)$
152	147 149 151	cnmpt1t	$⊢ φ \to (z \in ⋃ J ⟼ ⟨{z ↾}_{A}, {z ↾}_{B}⟩) \in (J Cn (K \times_{t} L))$
153	141 152	eqeltrd	$⊢ φ \to G^{-1} \in (J Cn (K \times_{t} L))$
154		ishmeo	$⊢ G \in ((K \times_{t} L) Homeo J) \leftrightarrow (G \in ((K \times_{t} L) Cn J) \land G^{-1} \in (J Cn (K \times_{t} L)))$
155	140 153 154	sylanbrc	$⊢ φ \to G \in ((K \times_{t} L) Homeo J)$

Metamath Proof Explorer

Theorem ptunhmeo

Proof