Theorem ptunhmeo 22100

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 (𝐴↑𝐵) · (𝐴↑𝐶) = 𝐴↑(𝐵 + 𝐶). (Contributed by Mario Carneiro, 8-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)

Hypotheses

Ref	Expression
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

Ref	Expression
ptunhmeo	⊢ (𝜑 → 𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜑,𝑥,𝑦   𝑥,𝐶,𝑦   𝑥,𝐹,𝑦   𝑥,𝐽,𝑦   𝑥,𝐾,𝑦   𝑥,𝐿,𝑦   𝑥,𝑋,𝑦   𝑥,𝑌,𝑦

Allowed substitution hints:   𝐺(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem ptunhmeo

Dummy variables 𝑓 𝑘 𝑛 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptunhmeo.g	. . . . 5 ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥 ∪ 𝑦))
2		vex 3439	. . . . . . . 8 ⊢ 𝑥 ∈ V
3		vex 3439	. . . . . . . 8 ⊢ 𝑦 ∈ V
4	2, 3	op1std 7558	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑧) = 𝑥)
5	2, 3	op2ndd 7559	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
6	4, 5	uneq12d 4063	. . . . . 6 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = (𝑥 ∪ 𝑦))
7	6	mpompt 7125	. . . . 5 ⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑧) ∪ (2nd ‘𝑧))) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥 ∪ 𝑦))
8	1, 7	eqtr4i 2821	. . . 4 ⊢ 𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑧) ∪ (2nd ‘𝑧)))
9		xp1st 7580	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑋 × 𝑌) → (1st ‘𝑧) ∈ 𝑋)
10	9	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st ‘𝑧) ∈ 𝑋)
11		ixpeq2 8327	. . . . . . . . . . . . 13 ⊢ (∀𝑛 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑛) = ∪ (𝐹‘𝑛) → X𝑛 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑛) = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛))
12		fvres 6560	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑛) = (𝐹‘𝑛))
13	12	unieqd 4757	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ 𝐴 → ∪ ((𝐹 ↾ 𝐴)‘𝑛) = ∪ (𝐹‘𝑛))
14	11, 13	mprg 3118	. . . . . . . . . . . 12 ⊢ X𝑛 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑛) = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
15		ptunhmeo.c	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
16		ssun1 4071	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
17		ptunhmeo.u	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐶 = (𝐴 ∪ 𝐵))
18	16, 17	sseqtrrid 3943	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
19	15, 18	ssexd 5122	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐴 ∈ V)
20		ptunhmeo.f	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:𝐶⟶Top)
21	20, 18	fssresd 6416	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶Top)
22		ptunhmeo.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (∏t‘(𝐹 ↾ 𝐴))
23	22	ptuni 21886	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ V ∧ (𝐹 ↾ 𝐴):𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑛) = ∪ 𝐾)
24	19, 21, 23	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑛 ∈ 𝐴 ∪ ((𝐹 ↾ 𝐴)‘𝑛) = ∪ 𝐾)
25	14, 24	syl5eqr 2844	. . . . . . . . . . 11 ⊢ (𝜑 → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = ∪ 𝐾)
26		ptunhmeo.x	. . . . . . . . . . 11 ⊢ 𝑋 = ∪ 𝐾
27	25, 26	syl6eqr 2848	. . . . . . . . . 10 ⊢ (𝜑 → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = 𝑋)
28	27	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = 𝑋)
29	10, 28	eleqtrrd 2885	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st ‘𝑧) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛))
30		xp2nd 7581	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑋 × 𝑌) → (2nd ‘𝑧) ∈ 𝑌)
31	30	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) ∈ 𝑌)
32	17	eqcomd 2800	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝐶)
33		ptunhmeo.i	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)
34		uneqdifeq 4354	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵))
35	18, 33, 34	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵))
36	32, 35	mpbid 233	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶 ∖ 𝐴) = 𝐵)
37	36	ixpeq1d 8325	. . . . . . . . . . 11 ⊢ (𝜑 → X𝑛 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑛) = X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛))
38		ixpeq2 8327	. . . . . . . . . . . . . 14 ⊢ (∀𝑛 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑛) = ∪ (𝐹‘𝑛) → X𝑛 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑛) = X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛))
39		fvres 6560	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑛) = (𝐹‘𝑛))
40	39	unieqd 4757	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ 𝐵 → ∪ ((𝐹 ↾ 𝐵)‘𝑛) = ∪ (𝐹‘𝑛))
41	38, 40	mprg 3118	. . . . . . . . . . . . 13 ⊢ X𝑛 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑛) = X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛)
42		ssun2 4072	. . . . . . . . . . . . . . . 16 ⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵)
43	42, 17	sseqtrrid 3943	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
44	15, 43	ssexd 5122	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ V)
45	20, 43	fssresd 6416	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ↾ 𝐵):𝐵⟶Top)
46		ptunhmeo.l	. . . . . . . . . . . . . . 15 ⊢ 𝐿 = (∏t‘(𝐹 ↾ 𝐵))
47	46	ptuni 21886	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) → X𝑛 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑛) = ∪ 𝐿)
48	44, 45, 47	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → X𝑛 ∈ 𝐵 ∪ ((𝐹 ↾ 𝐵)‘𝑛) = ∪ 𝐿)
49	41, 48	syl5eqr 2844	. . . . . . . . . . . 12 ⊢ (𝜑 → X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛) = ∪ 𝐿)
50		ptunhmeo.y	. . . . . . . . . . . 12 ⊢ 𝑌 = ∪ 𝐿
51	49, 50	syl6eqr 2848	. . . . . . . . . . 11 ⊢ (𝜑 → X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛) = 𝑌)
52	37, 51	eqtrd 2830	. . . . . . . . . 10 ⊢ (𝜑 → X𝑛 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑛) = 𝑌)
53	52	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑛) = 𝑌)
54	31, 53	eleqtrrd 2885	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) ∈ X𝑛 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑛))
55	18	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝐴 ⊆ 𝐶)
56		undifixp 8349	. . . . . . . 8 ⊢ (((1st ‘𝑧) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∧ (2nd ‘𝑧) ∈ X𝑛 ∈ (𝐶 ∖ 𝐴)∪ (𝐹‘𝑛) ∧ 𝐴 ⊆ 𝐶) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ X𝑛 ∈ 𝐶 ∪ (𝐹‘𝑛))
57	29, 54, 55, 56	syl3anc 1364	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ X𝑛 ∈ 𝐶 ∪ (𝐹‘𝑛))
58		ixpfn 8319	. . . . . . 7 ⊢ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ X𝑛 ∈ 𝐶 ∪ (𝐹‘𝑛) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) Fn 𝐶)
59	57, 58	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) Fn 𝐶)
60		dffn5 6595	. . . . . 6 ⊢ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) Fn 𝐶 ↔ ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = (𝑘 ∈ 𝐶 ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘)))
61	59, 60	sylib 219	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → ((1st ‘𝑧) ∪ (2nd ‘𝑧)) = (𝑘 ∈ 𝐶 ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘)))
62	61	mpteq2dva 5058	. . . 4 ⊢ (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑧) ∪ (2nd ‘𝑧))) = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘 ∈ 𝐶 ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘))))
63	8, 62	syl5eq 2842	. . 3 ⊢ (𝜑 → 𝐺 = (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘 ∈ 𝐶 ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘))))
64		ptunhmeo.j	. . . 4 ⊢ 𝐽 = (∏t‘𝐹)
65		pttop 21874	. . . . . . . 8 ⊢ ((𝐴 ∈ V ∧ (𝐹 ↾ 𝐴):𝐴⟶Top) → (∏t‘(𝐹 ↾ 𝐴)) ∈ Top)
66	19, 21, 65	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (∏t‘(𝐹 ↾ 𝐴)) ∈ Top)
67	22, 66	syl5eqel 2886	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ Top)
68	26	toptopon 21209	. . . . . 6 ⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑋))
69	67, 68	sylib 219	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋))
70		pttop 21874	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top) → (∏t‘(𝐹 ↾ 𝐵)) ∈ Top)
71	44, 45, 70	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (∏t‘(𝐹 ↾ 𝐵)) ∈ Top)
72	46, 71	syl5eqel 2886	. . . . . 6 ⊢ (𝜑 → 𝐿 ∈ Top)
73	50	toptopon 21209	. . . . . 6 ⊢ (𝐿 ∈ Top ↔ 𝐿 ∈ (TopOn‘𝑌))
74	72, 73	sylib 219	. . . . 5 ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌))
75		txtopon 21883	. . . . 5 ⊢ ((𝐾 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (TopOn‘𝑌)) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
76	69, 74, 75	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
77	17	eleq2d 2867	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ 𝐶 ↔ 𝑘 ∈ (𝐴 ∪ 𝐵)))
78	77	biimpa 477	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → 𝑘 ∈ (𝐴 ∪ 𝐵))
79		elun 4048	. . . . . 6 ⊢ (𝑘 ∈ (𝐴 ∪ 𝐵) ↔ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵))
80	78, 79	sylib 219	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵))
81		ixpfn 8319	. . . . . . . . . . 11 ⊢ ((1st ‘𝑧) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) → (1st ‘𝑧) Fn 𝐴)
82	29, 81	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st ‘𝑧) Fn 𝐴)
83	82	adantlr 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st ‘𝑧) Fn 𝐴)
84	51	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛) = 𝑌)
85	31, 84	eleqtrrd 2885	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) ∈ X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛))
86		ixpfn 8319	. . . . . . . . . . 11 ⊢ ((2nd ‘𝑧) ∈ X𝑛 ∈ 𝐵 ∪ (𝐹‘𝑛) → (2nd ‘𝑧) Fn 𝐵)
87	85, 86	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) Fn 𝐵)
88	87	adantlr 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) Fn 𝐵)
89	33	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴 ∩ 𝐵) = ∅)
90		simplr 765	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘 ∈ 𝐴)
91		fvun1 6624	. . . . . . . . 9 ⊢ (((1st ‘𝑧) Fn 𝐴 ∧ (2nd ‘𝑧) Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑘 ∈ 𝐴)) → (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘) = ((1st ‘𝑧)‘𝑘))
92	83, 88, 89, 90, 91	syl112anc 1367	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘) = ((1st ‘𝑧)‘𝑘))
93	92	mpteq2dva 5058	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑧)‘𝑘)))
94	76	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
95	4	mpompt 7125	. . . . . . . . 9 ⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑧)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥)
96	69	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐾 ∈ (TopOn‘𝑋))
97	74	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐿 ∈ (TopOn‘𝑌))
98	96, 97	cnmpt1st 21960	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑥) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
99	95, 98	syl5eqel 2886	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (1st ‘𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐾))
100	19	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐴 ∈ V)
101	21	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹 ↾ 𝐴):𝐴⟶Top)
102		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴)
103	26, 22	ptpjcn 21903	. . . . . . . . . 10 ⊢ ((𝐴 ∈ V ∧ (𝐹 ↾ 𝐴):𝐴⟶Top ∧ 𝑘 ∈ 𝐴) → (𝑓 ∈ 𝑋 ↦ (𝑓‘𝑘)) ∈ (𝐾 Cn ((𝐹 ↾ 𝐴)‘𝑘)))
104	100, 101, 102, 103	syl3anc 1364	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑓 ∈ 𝑋 ↦ (𝑓‘𝑘)) ∈ (𝐾 Cn ((𝐹 ↾ 𝐴)‘𝑘)))
105		fvres 6560	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑘) = (𝐹‘𝑘))
106	105	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹 ↾ 𝐴)‘𝑘) = (𝐹‘𝑘))
107	106	oveq2d 7035	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐾 Cn ((𝐹 ↾ 𝐴)‘𝑘)) = (𝐾 Cn (𝐹‘𝑘)))
108	104, 107	eleqtrd 2884	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑓 ∈ 𝑋 ↦ (𝑓‘𝑘)) ∈ (𝐾 Cn (𝐹‘𝑘)))
109		fveq1 6540	. . . . . . . 8 ⊢ (𝑓 = (1st ‘𝑧) → (𝑓‘𝑘) = ((1st ‘𝑧)‘𝑘))
110	94, 99, 96, 108, 109	cnmpt11 21955	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((1st ‘𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘)))
111	93, 110	eqeltrd 2882	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘)))
112	82	adantlr 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (1st ‘𝑧) Fn 𝐴)
113	87	adantlr 711	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (2nd ‘𝑧) Fn 𝐵)
114	33	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (𝐴 ∩ 𝐵) = ∅)
115		simplr 765	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → 𝑘 ∈ 𝐵)
116		fvun2 6625	. . . . . . . . 9 ⊢ (((1st ‘𝑧) Fn 𝐴 ∧ (2nd ‘𝑧) Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑘 ∈ 𝐵)) → (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘) = ((2nd ‘𝑧)‘𝑘))
117	112, 113, 114, 115, 116	syl112anc 1367	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑧 ∈ (𝑋 × 𝑌)) → (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘) = ((2nd ‘𝑧)‘𝑘))
118	117	mpteq2dva 5058	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘)) = (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd ‘𝑧)‘𝑘)))
119	76	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝐾 ×t 𝐿) ∈ (TopOn‘(𝑋 × 𝑌)))
120	5	mpompt 7125	. . . . . . . . 9 ⊢ (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦)
121	69	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐾 ∈ (TopOn‘𝑋))
122	74	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐿 ∈ (TopOn‘𝑌))
123	121, 122	cnmpt2nd 21961	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝑦) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
124	120, 123	syl5eqel 2886	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (2nd ‘𝑧)) ∈ ((𝐾 ×t 𝐿) Cn 𝐿))
125	44	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝐵 ∈ V)
126	45	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝐹 ↾ 𝐵):𝐵⟶Top)
127		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵)
128	50, 46	ptpjcn 21903	. . . . . . . . . 10 ⊢ ((𝐵 ∈ V ∧ (𝐹 ↾ 𝐵):𝐵⟶Top ∧ 𝑘 ∈ 𝐵) → (𝑓 ∈ 𝑌 ↦ (𝑓‘𝑘)) ∈ (𝐿 Cn ((𝐹 ↾ 𝐵)‘𝑘)))
129	125, 126, 127, 128	syl3anc 1364	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑓 ∈ 𝑌 ↦ (𝑓‘𝑘)) ∈ (𝐿 Cn ((𝐹 ↾ 𝐵)‘𝑘)))
130		fvres 6560	. . . . . . . . . . 11 ⊢ (𝑘 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑘) = (𝐹‘𝑘))
131	130	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ((𝐹 ↾ 𝐵)‘𝑘) = (𝐹‘𝑘))
132	131	oveq2d 7035	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝐿 Cn ((𝐹 ↾ 𝐵)‘𝑘)) = (𝐿 Cn (𝐹‘𝑘)))
133	129, 132	eleqtrd 2884	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑓 ∈ 𝑌 ↦ (𝑓‘𝑘)) ∈ (𝐿 Cn (𝐹‘𝑘)))
134		fveq1 6540	. . . . . . . 8 ⊢ (𝑓 = (2nd ‘𝑧) → (𝑓‘𝑘) = ((2nd ‘𝑧)‘𝑘))
135	119, 124, 122, 133, 134	cnmpt11 21955	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ ((2nd ‘𝑧)‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘)))
136	118, 135	eqeltrd 2882	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘)))
137	111, 136	jaodan 952	. . . . 5 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∨ 𝑘 ∈ 𝐵)) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘)))
138	80, 137	syldan 591	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐶) → (𝑧 ∈ (𝑋 × 𝑌) ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘)) ∈ ((𝐾 ×t 𝐿) Cn (𝐹‘𝑘)))
139	64, 76, 15, 20, 138	ptcn 21919	. . 3 ⊢ (𝜑 → (𝑧 ∈ (𝑋 × 𝑌) ↦ (𝑘 ∈ 𝐶 ↦ (((1st ‘𝑧) ∪ (2nd ‘𝑧))‘𝑘))) ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
140	63, 139	eqeltrd 2882	. 2 ⊢ (𝜑 → 𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽))
141	26, 50, 64, 22, 46, 1, 15, 20, 17, 33	ptuncnv 22099	. . 3 ⊢ (𝜑 → ◡𝐺 = (𝑧 ∈ ∪ 𝐽 ↦ ⟨(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)⟩))
142		pttop 21874	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐹:𝐶⟶Top) → (∏t‘𝐹) ∈ Top)
143	15, 20, 142	syl2anc 584	. . . . . 6 ⊢ (𝜑 → (∏t‘𝐹) ∈ Top)
144	64, 143	syl5eqel 2886	. . . . 5 ⊢ (𝜑 → 𝐽 ∈ Top)
145		eqid 2794	. . . . . 6 ⊢ ∪ 𝐽 = ∪ 𝐽
146	145	toptopon 21209	. . . . 5 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))
147	144, 146	sylib 219	. . . 4 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽))
148	145, 64, 22	ptrescn 21931	. . . . 5 ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐹:𝐶⟶Top ∧ 𝐴 ⊆ 𝐶) → (𝑧 ∈ ∪ 𝐽 ↦ (𝑧 ↾ 𝐴)) ∈ (𝐽 Cn 𝐾))
149	15, 20, 18, 148	syl3anc 1364	. . . 4 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝐽 ↦ (𝑧 ↾ 𝐴)) ∈ (𝐽 Cn 𝐾))
150	145, 64, 46	ptrescn 21931	. . . . 5 ⊢ ((𝐶 ∈ 𝑉 ∧ 𝐹:𝐶⟶Top ∧ 𝐵 ⊆ 𝐶) → (𝑧 ∈ ∪ 𝐽 ↦ (𝑧 ↾ 𝐵)) ∈ (𝐽 Cn 𝐿))
151	15, 20, 43, 150	syl3anc 1364	. . . 4 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝐽 ↦ (𝑧 ↾ 𝐵)) ∈ (𝐽 Cn 𝐿))
152	147, 149, 151	cnmpt1t 21957	. . 3 ⊢ (𝜑 → (𝑧 ∈ ∪ 𝐽 ↦ ⟨(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)⟩) ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
153	141, 152	eqeltrd 2882	. 2 ⊢ (𝜑 → ◡𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿)))
154		ishmeo 22051	. 2 ⊢ (𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽) ↔ (𝐺 ∈ ((𝐾 ×t 𝐿) Cn 𝐽) ∧ ◡𝐺 ∈ (𝐽 Cn (𝐾 ×t 𝐿))))
155	140, 153, 154	sylanbrc 583	1 ⊢ (𝜑 → 𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 842   = wceq 1522   ∈ wcel 2080  Vcvv 3436   ∖ cdif 3858   ∪ cun 3859   ∩ cin 3860   ⊆ wss 3861  ∅c0 4213  ⟨cop 4480  ∪ cuni 4747   ↦ cmpt 5043   × cxp 5444  ^◡ccnv 5445   ↾ cres 5448   Fn wfn 6223  ⟶wf 6224  ‘cfv 6228  (class class class)co 7019   ∈ cmpo 7021  1^st c1st 7546  2^nd c2nd 7547  Xcixp 8313  ∏_tcpt 16541  Topctop 21185  TopOnctopon 21202   Cn ccn 21516   ×_t ctx 21852  Homeochmeo 22045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-ral 3109  df-rex 3110  df-reu 3111  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-int 4785  df-iun 4829  df-iin 4830  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-pred 6026  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-ov 7022  df-oprab 7023  df-mpo 7024  df-om 7440  df-1st 7548  df-2nd 7549  df-wrecs 7801  df-recs 7863  df-rdg 7901  df-1o 7956  df-oadd 7960  df-er 8142  df-map 8261  df-ixp 8314  df-en 8361  df-dom 8362  df-fin 8364  df-fi 8724  df-topgen 16546  df-pt 16547  df-top 21186  df-topon 21203  df-bases 21238  df-cn 21519  df-cnp 21520  df-tx 21854  df-hmeo 22047

This theorem is referenced by:  xpstopnlem1  22101  ptcmpfi  22105