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	⊢ 𝑋 = ∪ 𝐾
	ptunhmeo.y	⊢ 𝑌 = ∪ 𝐿
	ptunhmeo.j	⊢ 𝐽 = ( ∏_t ‘ 𝐹 )
	ptunhmeo.k	⊢ 𝐾 = ( ∏_t ‘ ( 𝐹 ↾ 𝐴 ) )
	ptunhmeo.l	⊢ 𝐿 = ( ∏_t ‘ ( 𝐹 ↾ 𝐵 ) )
	ptunhmeo.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 ∪ 𝑦 ) )
	ptunhmeo.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	ptunhmeo.f	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ Top )
	ptunhmeo.u	⊢ ( 𝜑 → 𝐶 = ( 𝐴 ∪ 𝐵 ) )
	ptunhmeo.i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
Assertion	ptunhmeo	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐾 ×_t 𝐿 ) Homeo 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		ptunhmeo.x	⊢ 𝑋 = ∪ 𝐾
2		ptunhmeo.y	⊢ 𝑌 = ∪ 𝐿
3		ptunhmeo.j	⊢ 𝐽 = ( ∏_t ‘ 𝐹 )
4		ptunhmeo.k	⊢ 𝐾 = ( ∏_t ‘ ( 𝐹 ↾ 𝐴 ) )
5		ptunhmeo.l	⊢ 𝐿 = ( ∏_t ‘ ( 𝐹 ↾ 𝐵 ) )
6		ptunhmeo.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 ∪ 𝑦 ) )
7		ptunhmeo.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8		ptunhmeo.f	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ Top )
9		ptunhmeo.u	⊢ ( 𝜑 → 𝐶 = ( 𝐴 ∪ 𝐵 ) )
10		ptunhmeo.i	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
11		vex	⊢ 𝑥 ∈ V
12		vex	⊢ 𝑦 ∈ V
13	11 12	op1std	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑧 ) = 𝑥 )
14	11 12	op2ndd	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑧 ) = 𝑦 )
15	13 14	uneq12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( 𝑥 ∪ 𝑦 ) )
16	15	mpompt	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( 𝑥 ∪ 𝑦 ) )
17	6 16	eqtr4i	⊢ 𝐺 = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) )
18		xp1st	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( 1^st ‘ 𝑧 ) ∈ 𝑋 )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 1^st ‘ 𝑧 ) ∈ 𝑋 )
20		ixpeq2	⊢ ( ∀ 𝑛 ∈ 𝐴 ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) → X 𝑛 ∈ 𝐴 ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑛 ) = X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) )
21		fvres	⊢ ( 𝑛 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
22	21	unieqd	⊢ ( 𝑛 ∈ 𝐴 → ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) )
23	20 22	mprg	⊢ X 𝑛 ∈ 𝐴 ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑛 ) = X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 )
24		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
25	24 9	sseqtrrid	⊢ ( 𝜑 → 𝐴 ⊆ 𝐶 )
26	7 25	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
27	8 25	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ Top )
28	4	ptuni	⊢ ( ( 𝐴 ∈ V ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ Top ) → X 𝑛 ∈ 𝐴 ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑛 ) = ∪ 𝐾 )
29	26 27 28	syl2anc	⊢ ( 𝜑 → X 𝑛 ∈ 𝐴 ∪ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑛 ) = ∪ 𝐾 )
30	23 29	eqtr3id	⊢ ( 𝜑 → X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = ∪ 𝐾 )
31	30 1	eqtr4di	⊢ ( 𝜑 → X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = 𝑋 )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = 𝑋 )
33	19 32	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 1^st ‘ 𝑧 ) ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) )
34		xp2nd	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( 2^nd ‘ 𝑧 ) ∈ 𝑌 )
35	34	adantl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑧 ) ∈ 𝑌 )
36	9	eqcomd	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = 𝐶 )
37		uneqdifeq	⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 ↔ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
38	25 10 37	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 ↔ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
39	36 38	mpbid	⊢ ( 𝜑 → ( 𝐶 ∖ 𝐴 ) = 𝐵 )
40	39	ixpeq1d	⊢ ( 𝜑 → X 𝑛 ∈ ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐹 ‘ 𝑛 ) = X 𝑛 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑛 ) )
41		ixpeq2	⊢ ( ∀ 𝑛 ∈ 𝐵 ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) → X 𝑛 ∈ 𝐵 ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑛 ) = X 𝑛 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑛 ) )
42		fvres	⊢ ( 𝑛 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
43	42	unieqd	⊢ ( 𝑛 ∈ 𝐵 → ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑛 ) )
44	41 43	mprg	⊢ X 𝑛 ∈ 𝐵 ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑛 ) = X 𝑛 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑛 )
45		ssun2	⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
46	45 9	sseqtrrid	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
47	7 46	ssexd	⊢ ( 𝜑 → 𝐵 ∈ V )
48	8 46	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ Top )
49	5	ptuni	⊢ ( ( 𝐵 ∈ V ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ Top ) → X 𝑛 ∈ 𝐵 ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑛 ) = ∪ 𝐿 )
50	47 48 49	syl2anc	⊢ ( 𝜑 → X 𝑛 ∈ 𝐵 ∪ ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑛 ) = ∪ 𝐿 )
51	44 50	eqtr3id	⊢ ( 𝜑 → X 𝑛 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑛 ) = ∪ 𝐿 )
52	51 2	eqtr4di	⊢ ( 𝜑 → X 𝑛 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑛 ) = 𝑌 )
53	40 52	eqtrd	⊢ ( 𝜑 → X 𝑛 ∈ ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐹 ‘ 𝑛 ) = 𝑌 )
54	53	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑛 ∈ ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐹 ‘ 𝑛 ) = 𝑌 )
55	35 54	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑧 ) ∈ X 𝑛 ∈ ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐹 ‘ 𝑛 ) )
56	25	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → 𝐴 ⊆ 𝐶 )
57		undifixp	⊢ ( ( ( 1^st ‘ 𝑧 ) ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ∧ ( 2^nd ‘ 𝑧 ) ∈ X 𝑛 ∈ ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐹 ‘ 𝑛 ) ∧ 𝐴 ⊆ 𝐶 ) → ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ X 𝑛 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑛 ) )
58	33 55 56 57	syl3anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ X 𝑛 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑛 ) )
59		ixpfn	⊢ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ X 𝑛 ∈ 𝐶 ∪ ( 𝐹 ‘ 𝑛 ) → ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) Fn 𝐶 )
60	58 59	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) Fn 𝐶 )
61		dffn5	⊢ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) Fn 𝐶 ↔ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( 𝑘 ∈ 𝐶 ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) )
62	60 61	sylib	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( 𝑘 ∈ 𝐶 ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) )
63	62	mpteq2dva	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑘 ∈ 𝐶 ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) ) )
64	17 63	syl5eq	⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑘 ∈ 𝐶 ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) ) )
65		pttop	⊢ ( ( 𝐴 ∈ V ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ Top ) → ( ∏_t ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ Top )
66	26 27 65	syl2anc	⊢ ( 𝜑 → ( ∏_t ‘ ( 𝐹 ↾ 𝐴 ) ) ∈ Top )
67	4 66	eqeltrid	⊢ ( 𝜑 → 𝐾 ∈ Top )
68	1	toptopon	⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
69	67 68	sylib	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
70		pttop	⊢ ( ( 𝐵 ∈ V ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ Top ) → ( ∏_t ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ Top )
71	47 48 70	syl2anc	⊢ ( 𝜑 → ( ∏_t ‘ ( 𝐹 ↾ 𝐵 ) ) ∈ Top )
72	5 71	eqeltrid	⊢ ( 𝜑 → 𝐿 ∈ Top )
73	2	toptopon	⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
74	72 73	sylib	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
75		txtopon	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐾 ×_t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
76	69 74 75	syl2anc	⊢ ( 𝜑 → ( 𝐾 ×_t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
77	9	eleq2d	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐶 ↔ 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ) )
78	77	biimpa	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) )
79		elun	⊢ ( 𝑘 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) )
80	78 79	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) )
81		ixpfn	⊢ ( ( 1^st ‘ 𝑧 ) ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) → ( 1^st ‘ 𝑧 ) Fn 𝐴 )
82	33 81	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 1^st ‘ 𝑧 ) Fn 𝐴 )
83	82	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 1^st ‘ 𝑧 ) Fn 𝐴 )
84	52	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → X 𝑛 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑛 ) = 𝑌 )
85	35 84	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑧 ) ∈ X 𝑛 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑛 ) )
86		ixpfn	⊢ ( ( 2^nd ‘ 𝑧 ) ∈ X 𝑛 ∈ 𝐵 ∪ ( 𝐹 ‘ 𝑛 ) → ( 2^nd ‘ 𝑧 ) Fn 𝐵 )
87	85 86	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑧 ) Fn 𝐵 )
88	87	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑧 ) Fn 𝐵 )
89	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
90		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → 𝑘 ∈ 𝐴 )
91		fvun1	⊢ ( ( ( 1^st ‘ 𝑧 ) Fn 𝐴 ∧ ( 2^nd ‘ 𝑧 ) Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑘 ∈ 𝐴 ) ) → ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) = ( ( 1^st ‘ 𝑧 ) ‘ 𝑘 ) )
92	83 88 89 90 91	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) = ( ( 1^st ‘ 𝑧 ) ‘ 𝑘 ) )
93	92	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ 𝑧 ) ‘ 𝑘 ) ) )
94	76	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐾 ×_t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
95	13	mpompt	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1^st ‘ 𝑧 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑥 )
96	69	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
97	74	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
98	96 97	cnmpt1st	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑥 ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn 𝐾 ) )
99	95 98	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1^st ‘ 𝑧 ) ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn 𝐾 ) )
100	26	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐴 ∈ V )
101	27	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ Top )
102		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑘 ∈ 𝐴 )
103	1 4	ptpjcn	⊢ ( ( 𝐴 ∈ V ∧ ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ Top ∧ 𝑘 ∈ 𝐴 ) → ( 𝑓 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ ( 𝐾 Cn ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) ) )
104	100 101 102 103	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑓 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ ( 𝐾 Cn ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) ) )
105		fvres	⊢ ( 𝑘 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
106	105	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
107	106	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐾 Cn ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑘 ) ) = ( 𝐾 Cn ( 𝐹 ‘ 𝑘 ) ) )
108	104 107	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑓 ∈ 𝑋 ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ ( 𝐾 Cn ( 𝐹 ‘ 𝑘 ) ) )
109		fveq1	⊢ ( 𝑓 = ( 1^st ‘ 𝑧 ) → ( 𝑓 ‘ 𝑘 ) = ( ( 1^st ‘ 𝑧 ) ‘ 𝑘 ) )
110	94 99 96 108 109	cnmpt11	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ 𝑧 ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn ( 𝐹 ‘ 𝑘 ) ) )
111	93 110	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn ( 𝐹 ‘ 𝑘 ) ) )
112	82	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 1^st ‘ 𝑧 ) Fn 𝐴 )
113	87	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑧 ) Fn 𝐵 )
114	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
115		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → 𝑘 ∈ 𝐵 )
116		fvun2	⊢ ( ( ( 1^st ‘ 𝑧 ) Fn 𝐴 ∧ ( 2^nd ‘ 𝑧 ) Fn 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑘 ∈ 𝐵 ) ) → ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) = ( ( 2^nd ‘ 𝑧 ) ‘ 𝑘 ) )
117	112 113 114 115 116	syl112anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) = ( ( 2^nd ‘ 𝑧 ) ‘ 𝑘 ) )
118	117	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 2^nd ‘ 𝑧 ) ‘ 𝑘 ) ) )
119	76	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝐾 ×_t 𝐿 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
120	14	mpompt	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2^nd ‘ 𝑧 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑦 )
121	69	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) )
122	74	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐿 ∈ ( TopOn ‘ 𝑌 ) )
123	121 122	cnmpt2nd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑦 ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn 𝐿 ) )
124	120 123	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn 𝐿 ) )
125	47	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝐵 ∈ V )
126	48	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ Top )
127		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
128	2 5	ptpjcn	⊢ ( ( 𝐵 ∈ V ∧ ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ Top ∧ 𝑘 ∈ 𝐵 ) → ( 𝑓 ∈ 𝑌 ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ ( 𝐿 Cn ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) ) )
129	125 126 127 128	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑓 ∈ 𝑌 ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ ( 𝐿 Cn ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) ) )
130		fvres	⊢ ( 𝑘 ∈ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
131	130	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
132	131	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝐿 Cn ( ( 𝐹 ↾ 𝐵 ) ‘ 𝑘 ) ) = ( 𝐿 Cn ( 𝐹 ‘ 𝑘 ) ) )
133	129 132	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑓 ∈ 𝑌 ↦ ( 𝑓 ‘ 𝑘 ) ) ∈ ( 𝐿 Cn ( 𝐹 ‘ 𝑘 ) ) )
134		fveq1	⊢ ( 𝑓 = ( 2^nd ‘ 𝑧 ) → ( 𝑓 ‘ 𝑘 ) = ( ( 2^nd ‘ 𝑧 ) ‘ 𝑘 ) )
135	119 124 122 133 134	cnmpt11	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 2^nd ‘ 𝑧 ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn ( 𝐹 ‘ 𝑘 ) ) )
136	118 135	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn ( 𝐹 ‘ 𝑘 ) ) )
137	111 136	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵 ) ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn ( 𝐹 ‘ 𝑘 ) ) )
138	80 137	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐶 ) → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn ( 𝐹 ‘ 𝑘 ) ) )
139	3 76 7 8 138	ptcn	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 𝑘 ∈ 𝐶 ↦ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ‘ 𝑘 ) ) ) ∈ ( ( 𝐾 ×_t 𝐿 ) Cn 𝐽 ) )
140	64 139	eqeltrd	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐾 ×_t 𝐿 ) Cn 𝐽 ) )
141	1 2 3 4 5 6 7 8 9 10	ptuncnv	⊢ ( 𝜑 → ^◡ 𝐺 = ( 𝑧 ∈ ∪ 𝐽 ↦ ⟨ ( 𝑧 ↾ 𝐴 ) , ( 𝑧 ↾ 𝐵 ) ⟩ ) )
142		pttop	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 : 𝐶 ⟶ Top ) → ( ∏_t ‘ 𝐹 ) ∈ Top )
143	7 8 142	syl2anc	⊢ ( 𝜑 → ( ∏_t ‘ 𝐹 ) ∈ Top )
144	3 143	eqeltrid	⊢ ( 𝜑 → 𝐽 ∈ Top )
145		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
146	145	toptopon	⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
147	144 146	sylib	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
148	145 3 4	ptrescn	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 : 𝐶 ⟶ Top ∧ 𝐴 ⊆ 𝐶 ) → ( 𝑧 ∈ ∪ 𝐽 ↦ ( 𝑧 ↾ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
149	7 8 25 148	syl3anc	⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝐽 ↦ ( 𝑧 ↾ 𝐴 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
150	145 3 5	ptrescn	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 : 𝐶 ⟶ Top ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑧 ∈ ∪ 𝐽 ↦ ( 𝑧 ↾ 𝐵 ) ) ∈ ( 𝐽 Cn 𝐿 ) )
151	7 8 46 150	syl3anc	⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝐽 ↦ ( 𝑧 ↾ 𝐵 ) ) ∈ ( 𝐽 Cn 𝐿 ) )
152	147 149 151	cnmpt1t	⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝐽 ↦ ⟨ ( 𝑧 ↾ 𝐴 ) , ( 𝑧 ↾ 𝐵 ) ⟩ ) ∈ ( 𝐽 Cn ( 𝐾 ×_t 𝐿 ) ) )
153	141 152	eqeltrd	⊢ ( 𝜑 → ^◡ 𝐺 ∈ ( 𝐽 Cn ( 𝐾 ×_t 𝐿 ) ) )
154		ishmeo	⊢ ( 𝐺 ∈ ( ( 𝐾 ×_t 𝐿 ) Homeo 𝐽 ) ↔ ( 𝐺 ∈ ( ( 𝐾 ×_t 𝐿 ) Cn 𝐽 ) ∧ ^◡ 𝐺 ∈ ( 𝐽 Cn ( 𝐾 ×_t 𝐿 ) ) ) )
155	140 153 154	sylanbrc	⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐾 ×_t 𝐿 ) Homeo 𝐽 ) )

Metamath Proof Explorer

Theorem ptunhmeo

Proof