txhmeo - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > txhmeo		Structured version Visualization version GIF version

Theorem txhmeo 22862

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

**Hypotheses**
Ref	Expression
txhmeo.1	⊢ 𝑋 = ∪ 𝐽
txhmeo.2	⊢ 𝑌 = ∪ 𝐾
txhmeo.3	⊢ (𝜑 → 𝐹 ∈ (𝐽Homeo𝐿))
txhmeo.4	⊢ (𝜑 → 𝐺 ∈ (𝐾Homeo𝑀))

**Assertion**
Ref	Expression
txhmeo	⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) ∈ ((𝐽 ×_t 𝐾)Homeo(𝐿 ×_t 𝑀)))

Distinct variable groups: 𝑥,𝑦,𝐹 𝑥,𝐽,𝑦 𝑥,𝐾,𝑦 𝜑,𝑥,𝑦 𝑥,𝐺,𝑦 𝑥,𝐿,𝑦 𝑥,𝑋,𝑦 𝑥,𝑌,𝑦 𝑥,𝑀,𝑦

Proof of Theorem txhmeo Dummy variables 𝑣 𝑢 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		txhmeo.3	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ (𝐽Homeo𝐿))
2		hmeocn 22819	. . . . . 6 ⊢ (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹 ∈ (𝐽 Cn 𝐿))
3	1, 2	syl 17	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐿))
4		cntop1 22299	. . . . 5 ⊢ (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐽 ∈ Top)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → 𝐽 ∈ Top)
6		txhmeo.1	. . . . 5 ⊢ 𝑋 = ∪ 𝐽
7	6	toptopon 21974	. . . 4 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
8	5, 7	sylib 217	. . 3 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))
9		txhmeo.4	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ (𝐾Homeo𝑀))
10		hmeocn 22819	. . . . . 6 ⊢ (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺 ∈ (𝐾 Cn 𝑀))
11	9, 10	syl 17	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝑀))
12		cntop1 22299	. . . . 5 ⊢ (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐾 ∈ Top)
13	11, 12	syl 17	. . . 4 ⊢ (𝜑 → 𝐾 ∈ Top)
14		txhmeo.2	. . . . 5 ⊢ 𝑌 = ∪ 𝐾
15	14	toptopon 21974	. . . 4 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌))
16	13, 15	sylib 217	. . 3 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌))
17	8, 16	cnmpt1st 22727	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) ∈ ((𝐽 ×_t 𝐾) Cn 𝐽))
18	8, 16, 17, 3	cnmpt21f 22731	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐹‘𝑥)) ∈ ((𝐽 ×_t 𝐾) Cn 𝐿))
19	8, 16	cnmpt2nd 22728	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐽 ×_t 𝐾) Cn 𝐾))
20	8, 16, 19, 11	cnmpt21f 22731	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐺‘𝑦)) ∈ ((𝐽 ×_t 𝐾) Cn 𝑀))
21	8, 16, 18, 20	cnmpt2t 22732	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) ∈ ((𝐽 ×_t 𝐾) Cn (𝐿 ×_t 𝑀)))
22		vex 3426	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
23		vex 3426	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
24	22, 23	op1std 7814	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (1^st ‘𝑢) = 𝑥)
25	24	fveq2d 6760	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐹‘(1^st ‘𝑢)) = (𝐹‘𝑥))
26	22, 23	op2ndd 7815	. . . . . . . . . 10 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (2^nd ‘𝑢) = 𝑦)
27	26	fveq2d 6760	. . . . . . . . 9 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → (𝐺‘(2^nd ‘𝑢)) = (𝐺‘𝑦))
28	25, 27	opeq12d 4809	. . . . . . . 8 ⊢ (𝑢 = ⟨𝑥, 𝑦⟩ → ⟨(𝐹‘(1^st ‘𝑢)), (𝐺‘(2^nd ‘𝑢))⟩ = ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)
29	28	mpompt 7366	. . . . . . 7 ⊢ (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1^st ‘𝑢)), (𝐺‘(2^nd ‘𝑢))⟩) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩)
30	29	eqcomi 2747	. . . . . 6 ⊢ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) = (𝑢 ∈ (𝑋 × 𝑌) ↦ ⟨(𝐹‘(1^st ‘𝑢)), (𝐺‘(2^nd ‘𝑢))⟩)
31		eqid 2738	. . . . . . . . . 10 ⊢ ∪ 𝐿 = ∪ 𝐿
32	6, 31	cnf 22305	. . . . . . . . 9 ⊢ (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐹:𝑋⟶∪ 𝐿)
33	3, 32	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐹:𝑋⟶∪ 𝐿)
34		xp1st 7836	. . . . . . . 8 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (1^st ‘𝑢) ∈ 𝑋)
35		ffvelrn 6941	. . . . . . . 8 ⊢ ((𝐹:𝑋⟶∪ 𝐿 ∧ (1^st ‘𝑢) ∈ 𝑋) → (𝐹‘(1^st ‘𝑢)) ∈ ∪ 𝐿)
36	33, 34, 35	syl2an 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑋 × 𝑌)) → (𝐹‘(1^st ‘𝑢)) ∈ ∪ 𝐿)
37		eqid 2738	. . . . . . . . . 10 ⊢ ∪ 𝑀 = ∪ 𝑀
38	14, 37	cnf 22305	. . . . . . . . 9 ⊢ (𝐺 ∈ (𝐾 Cn 𝑀) → 𝐺:𝑌⟶∪ 𝑀)
39	11, 38	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐺:𝑌⟶∪ 𝑀)
40		xp2nd 7837	. . . . . . . 8 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (2^nd ‘𝑢) ∈ 𝑌)
41		ffvelrn 6941	. . . . . . . 8 ⊢ ((𝐺:𝑌⟶∪ 𝑀 ∧ (2^nd ‘𝑢) ∈ 𝑌) → (𝐺‘(2^nd ‘𝑢)) ∈ ∪ 𝑀)
42	39, 40, 41	syl2an 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑋 × 𝑌)) → (𝐺‘(2^nd ‘𝑢)) ∈ ∪ 𝑀)
43	36, 42	opelxpd 5618	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑋 × 𝑌)) → ⟨(𝐹‘(1^st ‘𝑢)), (𝐺‘(2^nd ‘𝑢))⟩ ∈ (∪ 𝐿 × ∪ 𝑀))
44	6, 31	hmeof1o 22823	. . . . . . . . . 10 ⊢ (𝐹 ∈ (𝐽Homeo𝐿) → 𝐹:𝑋–1-1-onto→∪ 𝐿)
45	1, 44	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝑋–1-1-onto→∪ 𝐿)
46		f1ocnv 6712	. . . . . . . . 9 ⊢ (𝐹:𝑋–1-1-onto→∪ 𝐿 → ^◡𝐹:∪ 𝐿–1-1-onto→𝑋)
47		f1of 6700	. . . . . . . . 9 ⊢ (^◡𝐹:∪ 𝐿–1-1-onto→𝑋 → ^◡𝐹:∪ 𝐿⟶𝑋)
48	45, 46, 47	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ^◡𝐹:∪ 𝐿⟶𝑋)
49		xp1st 7836	. . . . . . . 8 ⊢ (𝑣 ∈ (∪ 𝐿 × ∪ 𝑀) → (1^st ‘𝑣) ∈ ∪ 𝐿)
50		ffvelrn 6941	. . . . . . . 8 ⊢ ((^◡𝐹:∪ 𝐿⟶𝑋 ∧ (1^st ‘𝑣) ∈ ∪ 𝐿) → (^◡𝐹‘(1^st ‘𝑣)) ∈ 𝑋)
51	48, 49, 50	syl2an 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)) → (^◡𝐹‘(1^st ‘𝑣)) ∈ 𝑋)
52	14, 37	hmeof1o 22823	. . . . . . . . . 10 ⊢ (𝐺 ∈ (𝐾Homeo𝑀) → 𝐺:𝑌–1-1-onto→∪ 𝑀)
53	9, 52	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐺:𝑌–1-1-onto→∪ 𝑀)
54		f1ocnv 6712	. . . . . . . . 9 ⊢ (𝐺:𝑌–1-1-onto→∪ 𝑀 → ^◡𝐺:∪ 𝑀–1-1-onto→𝑌)
55		f1of 6700	. . . . . . . . 9 ⊢ (^◡𝐺:∪ 𝑀–1-1-onto→𝑌 → ^◡𝐺:∪ 𝑀⟶𝑌)
56	53, 54, 55	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ^◡𝐺:∪ 𝑀⟶𝑌)
57		xp2nd 7837	. . . . . . . 8 ⊢ (𝑣 ∈ (∪ 𝐿 × ∪ 𝑀) → (2^nd ‘𝑣) ∈ ∪ 𝑀)
58		ffvelrn 6941	. . . . . . . 8 ⊢ ((^◡𝐺:∪ 𝑀⟶𝑌 ∧ (2^nd ‘𝑣) ∈ ∪ 𝑀) → (^◡𝐺‘(2^nd ‘𝑣)) ∈ 𝑌)
59	56, 57, 58	syl2an 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)) → (^◡𝐺‘(2^nd ‘𝑣)) ∈ 𝑌)
60	51, 59	opelxpd 5618	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀)) → ⟨(^◡𝐹‘(1^st ‘𝑣)), (^◡𝐺‘(2^nd ‘𝑣))⟩ ∈ (𝑋 × 𝑌))
61	45	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → 𝐹:𝑋–1-1-onto→∪ 𝐿)
62	34	ad2antrl 724	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → (1^st ‘𝑢) ∈ 𝑋)
63	49	ad2antll 725	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → (1^st ‘𝑣) ∈ ∪ 𝐿)
64		f1ocnvfvb 7132	. . . . . . . . . 10 ⊢ ((𝐹:𝑋–1-1-onto→∪ 𝐿 ∧ (1^st ‘𝑢) ∈ 𝑋 ∧ (1^st ‘𝑣) ∈ ∪ 𝐿) → ((𝐹‘(1^st ‘𝑢)) = (1^st ‘𝑣) ↔ (^◡𝐹‘(1^st ‘𝑣)) = (1^st ‘𝑢)))
65	61, 62, 63, 64	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → ((𝐹‘(1^st ‘𝑢)) = (1^st ‘𝑣) ↔ (^◡𝐹‘(1^st ‘𝑣)) = (1^st ‘𝑢)))
66		eqcom 2745	. . . . . . . . 9 ⊢ ((1^st ‘𝑣) = (𝐹‘(1^st ‘𝑢)) ↔ (𝐹‘(1^st ‘𝑢)) = (1^st ‘𝑣))
67		eqcom 2745	. . . . . . . . 9 ⊢ ((1^st ‘𝑢) = (^◡𝐹‘(1^st ‘𝑣)) ↔ (^◡𝐹‘(1^st ‘𝑣)) = (1^st ‘𝑢))
68	65, 66, 67	3bitr4g 313	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → ((1^st ‘𝑣) = (𝐹‘(1^st ‘𝑢)) ↔ (1^st ‘𝑢) = (^◡𝐹‘(1^st ‘𝑣))))
69	53	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → 𝐺:𝑌–1-1-onto→∪ 𝑀)
70	40	ad2antrl 724	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → (2^nd ‘𝑢) ∈ 𝑌)
71	57	ad2antll 725	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → (2^nd ‘𝑣) ∈ ∪ 𝑀)
72		f1ocnvfvb 7132	. . . . . . . . . 10 ⊢ ((𝐺:𝑌–1-1-onto→∪ 𝑀 ∧ (2^nd ‘𝑢) ∈ 𝑌 ∧ (2^nd ‘𝑣) ∈ ∪ 𝑀) → ((𝐺‘(2^nd ‘𝑢)) = (2^nd ‘𝑣) ↔ (^◡𝐺‘(2^nd ‘𝑣)) = (2^nd ‘𝑢)))
73	69, 70, 71, 72	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → ((𝐺‘(2^nd ‘𝑢)) = (2^nd ‘𝑣) ↔ (^◡𝐺‘(2^nd ‘𝑣)) = (2^nd ‘𝑢)))
74		eqcom 2745	. . . . . . . . 9 ⊢ ((2^nd ‘𝑣) = (𝐺‘(2^nd ‘𝑢)) ↔ (𝐺‘(2^nd ‘𝑢)) = (2^nd ‘𝑣))
75		eqcom 2745	. . . . . . . . 9 ⊢ ((2^nd ‘𝑢) = (^◡𝐺‘(2^nd ‘𝑣)) ↔ (^◡𝐺‘(2^nd ‘𝑣)) = (2^nd ‘𝑢))
76	73, 74, 75	3bitr4g 313	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → ((2^nd ‘𝑣) = (𝐺‘(2^nd ‘𝑢)) ↔ (2^nd ‘𝑢) = (^◡𝐺‘(2^nd ‘𝑣))))
77	68, 76	anbi12d 630	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → (((1^st ‘𝑣) = (𝐹‘(1^st ‘𝑢)) ∧ (2^nd ‘𝑣) = (𝐺‘(2^nd ‘𝑢))) ↔ ((1^st ‘𝑢) = (^◡𝐹‘(1^st ‘𝑣)) ∧ (2^nd ‘𝑢) = (^◡𝐺‘(2^nd ‘𝑣)))))
78		eqop 7846	. . . . . . . 8 ⊢ (𝑣 ∈ (∪ 𝐿 × ∪ 𝑀) → (𝑣 = ⟨(𝐹‘(1^st ‘𝑢)), (𝐺‘(2^nd ‘𝑢))⟩ ↔ ((1^st ‘𝑣) = (𝐹‘(1^st ‘𝑢)) ∧ (2^nd ‘𝑣) = (𝐺‘(2^nd ‘𝑢)))))
79	78	ad2antll 725	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → (𝑣 = ⟨(𝐹‘(1^st ‘𝑢)), (𝐺‘(2^nd ‘𝑢))⟩ ↔ ((1^st ‘𝑣) = (𝐹‘(1^st ‘𝑢)) ∧ (2^nd ‘𝑣) = (𝐺‘(2^nd ‘𝑢)))))
80		eqop 7846	. . . . . . . 8 ⊢ (𝑢 ∈ (𝑋 × 𝑌) → (𝑢 = ⟨(^◡𝐹‘(1^st ‘𝑣)), (^◡𝐺‘(2^nd ‘𝑣))⟩ ↔ ((1^st ‘𝑢) = (^◡𝐹‘(1^st ‘𝑣)) ∧ (2^nd ‘𝑢) = (^◡𝐺‘(2^nd ‘𝑣)))))
81	80	ad2antrl 724	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → (𝑢 = ⟨(^◡𝐹‘(1^st ‘𝑣)), (^◡𝐺‘(2^nd ‘𝑣))⟩ ↔ ((1^st ‘𝑢) = (^◡𝐹‘(1^st ‘𝑣)) ∧ (2^nd ‘𝑢) = (^◡𝐺‘(2^nd ‘𝑣)))))
82	77, 79, 81	3bitr4rd 311	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ (𝑋 × 𝑌) ∧ 𝑣 ∈ (∪ 𝐿 × ∪ 𝑀))) → (𝑢 = ⟨(^◡𝐹‘(1^st ‘𝑣)), (^◡𝐺‘(2^nd ‘𝑣))⟩ ↔ 𝑣 = ⟨(𝐹‘(1^st ‘𝑢)), (𝐺‘(2^nd ‘𝑢))⟩))
83	30, 43, 60, 82	f1ocnv2d 7500	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩):(𝑋 × 𝑌)–1-1-onto→(∪ 𝐿 × ∪ 𝑀) ∧ ^◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) = (𝑣 ∈ (∪ 𝐿 × ∪ 𝑀) ↦ ⟨(^◡𝐹‘(1^st ‘𝑣)), (^◡𝐺‘(2^nd ‘𝑣))⟩)))
84	83	simprd 495	. . . 4 ⊢ (𝜑 → ^◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) = (𝑣 ∈ (∪ 𝐿 × ∪ 𝑀) ↦ ⟨(^◡𝐹‘(1^st ‘𝑣)), (^◡𝐺‘(2^nd ‘𝑣))⟩))
85		vex 3426	. . . . . . . 8 ⊢ 𝑧 ∈ V
86		vex 3426	. . . . . . . 8 ⊢ 𝑤 ∈ V
87	85, 86	op1std 7814	. . . . . . 7 ⊢ (𝑣 = ⟨𝑧, 𝑤⟩ → (1^st ‘𝑣) = 𝑧)
88	87	fveq2d 6760	. . . . . 6 ⊢ (𝑣 = ⟨𝑧, 𝑤⟩ → (^◡𝐹‘(1^st ‘𝑣)) = (^◡𝐹‘𝑧))
89	85, 86	op2ndd 7815	. . . . . . 7 ⊢ (𝑣 = ⟨𝑧, 𝑤⟩ → (2^nd ‘𝑣) = 𝑤)
90	89	fveq2d 6760	. . . . . 6 ⊢ (𝑣 = ⟨𝑧, 𝑤⟩ → (^◡𝐺‘(2^nd ‘𝑣)) = (^◡𝐺‘𝑤))
91	88, 90	opeq12d 4809	. . . . 5 ⊢ (𝑣 = ⟨𝑧, 𝑤⟩ → ⟨(^◡𝐹‘(1^st ‘𝑣)), (^◡𝐺‘(2^nd ‘𝑣))⟩ = ⟨(^◡𝐹‘𝑧), (^◡𝐺‘𝑤)⟩)
92	91	mpompt 7366	. . . 4 ⊢ (𝑣 ∈ (∪ 𝐿 × ∪ 𝑀) ↦ ⟨(^◡𝐹‘(1^st ‘𝑣)), (^◡𝐺‘(2^nd ‘𝑣))⟩) = (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ ⟨(^◡𝐹‘𝑧), (^◡𝐺‘𝑤)⟩)
93	84, 92	eqtrdi 2795	. . 3 ⊢ (𝜑 → ^◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) = (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ ⟨(^◡𝐹‘𝑧), (^◡𝐺‘𝑤)⟩))
94		cntop2 22300	. . . . . 6 ⊢ (𝐹 ∈ (𝐽 Cn 𝐿) → 𝐿 ∈ Top)
95	3, 94	syl 17	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ Top)
96	31	toptopon 21974	. . . . 5 ⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘∪ 𝐿))
97	95, 96	sylib 217	. . . 4 ⊢ (𝜑 → 𝐿 ∈ (TopOn‘∪ 𝐿))
98		cntop2 22300	. . . . . 6 ⊢ (𝐺 ∈ (𝐾 Cn 𝑀) → 𝑀 ∈ Top)
99	11, 98	syl 17	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ Top)
100	37	toptopon 21974	. . . . 5 ⊢ (𝑀 ∈ Top ↔ 𝑀 ∈ (TopOn‘∪ 𝑀))
101	99, 100	sylib 217	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (TopOn‘∪ 𝑀))
102	97, 101	cnmpt1st 22727	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 𝑧) ∈ ((𝐿 ×_t 𝑀) Cn 𝐿))
103		hmeocnvcn 22820	. . . . . 6 ⊢ (𝐹 ∈ (𝐽Homeo𝐿) → ^◡𝐹 ∈ (𝐿 Cn 𝐽))
104	1, 103	syl 17	. . . . 5 ⊢ (𝜑 → ^◡𝐹 ∈ (𝐿 Cn 𝐽))
105	97, 101, 102, 104	cnmpt21f 22731	. . . 4 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ (^◡𝐹‘𝑧)) ∈ ((𝐿 ×_t 𝑀) Cn 𝐽))
106	97, 101	cnmpt2nd 22728	. . . . 5 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ 𝑤) ∈ ((𝐿 ×_t 𝑀) Cn 𝑀))
107		hmeocnvcn 22820	. . . . . 6 ⊢ (𝐺 ∈ (𝐾Homeo𝑀) → ^◡𝐺 ∈ (𝑀 Cn 𝐾))
108	9, 107	syl 17	. . . . 5 ⊢ (𝜑 → ^◡𝐺 ∈ (𝑀 Cn 𝐾))
109	97, 101, 106, 108	cnmpt21f 22731	. . . 4 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ (^◡𝐺‘𝑤)) ∈ ((𝐿 ×_t 𝑀) Cn 𝐾))
110	97, 101, 105, 109	cnmpt2t 22732	. . 3 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝐿, 𝑤 ∈ ∪ 𝑀 ↦ ⟨(^◡𝐹‘𝑧), (^◡𝐺‘𝑤)⟩) ∈ ((𝐿 ×_t 𝑀) Cn (𝐽 ×_t 𝐾)))
111	93, 110	eqeltrd 2839	. 2 ⊢ (𝜑 → ^◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) ∈ ((𝐿 ×_t 𝑀) Cn (𝐽 ×_t 𝐾)))
112		ishmeo 22818	. 2 ⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) ∈ ((𝐽 ×_t 𝐾)Homeo(𝐿 ×_t 𝑀)) ↔ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) ∈ ((𝐽 ×_t 𝐾) Cn (𝐿 ×_t 𝑀)) ∧ ^◡(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) ∈ ((𝐿 ×_t 𝑀) Cn (𝐽 ×_t 𝐾))))
113	21, 111, 112	sylanbrc 582	1 ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) ∈ ((𝐽 ×_t 𝐾)Homeo(𝐿 ×_t 𝑀)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ⟨cop 4564 ∪ cuni 4836 ↦ cmpt 5153 × cxp 5578 ^◡ccnv 5579 ⟶wf 6414 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 ∈ cmpo 7257 1^st c1st 7802 2^nd c2nd 7803 Topctop 21950 TopOnctopon 21967 Cn ccn 22283 ×_t ctx 22619 Homeochmeo 22812

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-ov 7258 df-oprab 7259 df-mpo 7260 df-1st 7804 df-2nd 7805 df-map 8575 df-topgen 17071 df-top 21951 df-topon 21968 df-bases 22004 df-cn 22286 df-tx 22621 df-hmeo 22814

This theorem is referenced by: xpstopnlem1 22868

W3C validator