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	⊢ 𝑋 = ∪ 𝐽
	txhmeo.2	⊢ 𝑌 = ∪ 𝐾
	txhmeo.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Homeo 𝐿 ) )
	txhmeo.4	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Homeo 𝑀 ) )
Assertion	txhmeo	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑦 ) ⟩ ) ∈ ( ( 𝐽 ×_t 𝐾 ) Homeo ( 𝐿 ×_t 𝑀 ) ) )

Proof

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

Metamath Proof Explorer

Theorem txhmeo

Proof