xkohmeo

Description: The Exponential Law for topological spaces. The "currying" function F is a homeomorphism on function spaces when J and K are exponentiable spaces (by xkococn , it is sufficient to assume that J , K are locally compact to ensure exponentiability). (Contributed by Mario Carneiro, 13-Apr-2015) (Proof shortened by Mario Carneiro, 23-Aug-2015)

	Ref	Expression
Hypotheses	xkohmeo.x	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	xkohmeo.y	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
	xkohmeo.f	⊢ 𝐹 = ( 𝑓 ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) )
	xkohmeo.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑛-Locally Comp )
	xkohmeo.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Comp )
	xkohmeo.l	⊢ ( 𝜑 → 𝐿 ∈ Top )
Assertion	xkohmeo	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) Homeo ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xkohmeo.x	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		xkohmeo.y	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3		xkohmeo.f	⊢ 𝐹 = ( 𝑓 ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) )
4		xkohmeo.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑛-Locally Comp )
5		xkohmeo.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Comp )
6		xkohmeo.l	⊢ ( 𝜑 → 𝐿 ∈ Top )
7		txtopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
8	1 2 7	syl2anc	⊢ ( 𝜑 → ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
9		topontop	⊢ ( ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) → ( 𝐽 ×_t 𝐾 ) ∈ Top )
10	8 9	syl	⊢ ( 𝜑 → ( 𝐽 ×_t 𝐾 ) ∈ Top )
11		eqid	⊢ ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) = ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) )
12	11	xkotopon	⊢ ( ( ( 𝐽 ×_t 𝐾 ) ∈ Top ∧ 𝐿 ∈ Top ) → ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ∈ ( TopOn ‘ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) ) )
13	10 6 12	syl2anc	⊢ ( 𝜑 → ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ∈ ( TopOn ‘ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) ) )
14		vex	⊢ 𝑓 ∈ V
15		vex	⊢ 𝑥 ∈ V
16	14 15	op1std	⊢ ( 𝑧 = ⟨ 𝑓 , 𝑥 ⟩ → ( 1^st ‘ 𝑧 ) = 𝑓 )
17	14 15	op2ndd	⊢ ( 𝑧 = ⟨ 𝑓 , 𝑥 ⟩ → ( 2^nd ‘ 𝑧 ) = 𝑥 )
18		eqidd	⊢ ( 𝑧 = ⟨ 𝑓 , 𝑥 ⟩ → 𝑦 = 𝑦 )
19	16 17 18	oveq123d	⊢ ( 𝑧 = ⟨ 𝑓 , 𝑥 ⟩ → ( ( 2^nd ‘ 𝑧 ) ( 1^st ‘ 𝑧 ) 𝑦 ) = ( 𝑥 𝑓 𝑦 ) )
20	19	mpteq2dv	⊢ ( 𝑧 = ⟨ 𝑓 , 𝑥 ⟩ → ( 𝑦 ∈ 𝑌 ↦ ( ( 2^nd ‘ 𝑧 ) ( 1^st ‘ 𝑧 ) 𝑦 ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
21	20	mpompt	⊢ ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 𝑦 ∈ 𝑌 ↦ ( ( 2^nd ‘ 𝑧 ) ( 1^st ‘ 𝑧 ) 𝑦 ) ) ) = ( 𝑓 ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) , 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) )
22		txtopon	⊢ ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ∈ ( TopOn ‘ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ∈ ( TopOn ‘ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ) )
23	13 1 22	syl2anc	⊢ ( 𝜑 → ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ∈ ( TopOn ‘ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ) )
24		vex	⊢ 𝑧 ∈ V
25		vex	⊢ 𝑦 ∈ V
26	24 25	op1std	⊢ ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ → ( 1^st ‘ 𝑤 ) = 𝑧 )
27	26	fveq2d	⊢ ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) = ( 1^st ‘ 𝑧 ) )
28	26	fveq2d	⊢ ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) = ( 2^nd ‘ 𝑧 ) )
29	24 25	op2ndd	⊢ ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ → ( 2^nd ‘ 𝑤 ) = 𝑦 )
30	27 28 29	oveq123d	⊢ ( 𝑤 = ⟨ 𝑧 , 𝑦 ⟩ → ( ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ( 2^nd ‘ 𝑤 ) ) = ( ( 2^nd ‘ 𝑧 ) ( 1^st ‘ 𝑧 ) 𝑦 ) )
31	30	mpompt	⊢ ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ( 2^nd ‘ 𝑤 ) ) ) = ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) , 𝑦 ∈ 𝑌 ↦ ( ( 2^nd ‘ 𝑧 ) ( 1^st ‘ 𝑧 ) 𝑦 ) )
32		txtopon	⊢ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ∈ ( TopOn ‘ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) ∈ ( TopOn ‘ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ) )
33	23 2 32	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) ∈ ( TopOn ‘ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ) )
34		toptopon2	⊢ ( 𝐿 ∈ Top ↔ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
35	6 34	sylib	⊢ ( 𝜑 → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
36		txcmp	⊢ ( ( 𝑥 ∈ Comp ∧ 𝑦 ∈ Comp ) → ( 𝑥 ×_t 𝑦 ) ∈ Comp )
37	36	txnlly	⊢ ( ( 𝐽 ∈ 𝑛-Locally Comp ∧ 𝐾 ∈ 𝑛-Locally Comp ) → ( 𝐽 ×_t 𝐾 ) ∈ 𝑛-Locally Comp )
38	4 5 37	syl2anc	⊢ ( 𝜑 → ( 𝐽 ×_t 𝐾 ) ∈ 𝑛-Locally Comp )
39	27	mpompt	⊢ ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ) = ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) , 𝑦 ∈ 𝑌 ↦ ( 1^st ‘ 𝑧 ) )
40	8	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ) → ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
41	35	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ) → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
42		xp1st	⊢ ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) → ( 1^st ‘ 𝑤 ) ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ) → ( 1^st ‘ 𝑤 ) ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) )
44		xp1st	⊢ ( ( 1^st ‘ 𝑤 ) ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) → ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) )
45	43 44	syl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) )
46		cnf2	⊢ ( ( ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐿 )
47	40 41 45 46	syl3anc	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) : ( 𝑋 × 𝑌 ) ⟶ ∪ 𝐿 )
48	47	feqmptd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) = ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ‘ 𝑢 ) ) )
49	48	mpteq2dva	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ‘ 𝑢 ) ) ) )
50	39 49	eqtr3id	⊢ ( 𝜑 → ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) , 𝑦 ∈ 𝑌 ↦ ( 1^st ‘ 𝑧 ) ) = ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ‘ 𝑢 ) ) ) )
51	23 2	cnmpt1st	⊢ ( 𝜑 → ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) , 𝑦 ∈ 𝑌 ↦ 𝑧 ) ∈ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) Cn ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ) )
52		fveq2	⊢ ( 𝑡 = 𝑧 → ( 1^st ‘ 𝑡 ) = ( 1^st ‘ 𝑧 ) )
53	52	cbvmptv	⊢ ( 𝑡 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 1^st ‘ 𝑡 ) ) = ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 1^st ‘ 𝑧 ) )
54	16	mpompt	⊢ ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 1^st ‘ 𝑧 ) ) = ( 𝑓 ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) , 𝑥 ∈ 𝑋 ↦ 𝑓 )
55	13 1	cnmpt1st	⊢ ( 𝜑 → ( 𝑓 ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) , 𝑥 ∈ 𝑋 ↦ 𝑓 ) ∈ ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) Cn ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ) )
56	54 55	eqeltrid	⊢ ( 𝜑 → ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 1^st ‘ 𝑧 ) ) ∈ ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) Cn ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ) )
57	53 56	eqeltrid	⊢ ( 𝜑 → ( 𝑡 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 1^st ‘ 𝑡 ) ) ∈ ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) Cn ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ) )
58	23 2 51 23 57 52	cnmpt21	⊢ ( 𝜑 → ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) , 𝑦 ∈ 𝑌 ↦ ( 1^st ‘ 𝑧 ) ) ∈ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) Cn ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ) )
59	50 58	eqeltrrd	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ‘ 𝑢 ) ) ) ∈ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) Cn ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ) )
60	28	mpompt	⊢ ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) ) = ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) , 𝑦 ∈ 𝑌 ↦ ( 2^nd ‘ 𝑧 ) )
61		fveq2	⊢ ( 𝑡 = 𝑧 → ( 2^nd ‘ 𝑡 ) = ( 2^nd ‘ 𝑧 ) )
62	61	cbvmptv	⊢ ( 𝑡 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 2^nd ‘ 𝑡 ) ) = ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 2^nd ‘ 𝑧 ) )
63	17	mpompt	⊢ ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 2^nd ‘ 𝑧 ) ) = ( 𝑓 ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) , 𝑥 ∈ 𝑋 ↦ 𝑥 )
64	13 1	cnmpt2nd	⊢ ( 𝜑 → ( 𝑓 ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) , 𝑥 ∈ 𝑋 ↦ 𝑥 ) ∈ ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) Cn 𝐽 ) )
65	63 64	eqeltrid	⊢ ( 𝜑 → ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) Cn 𝐽 ) )
66	62 65	eqeltrid	⊢ ( 𝜑 → ( 𝑡 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 2^nd ‘ 𝑡 ) ) ∈ ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) Cn 𝐽 ) )
67	23 2 51 23 66 61	cnmpt21	⊢ ( 𝜑 → ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) , 𝑦 ∈ 𝑌 ↦ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) Cn 𝐽 ) )
68	60 67	eqeltrid	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) ) ∈ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) Cn 𝐽 ) )
69	29	mpompt	⊢ ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( 2^nd ‘ 𝑤 ) ) = ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) , 𝑦 ∈ 𝑌 ↦ 𝑦 )
70	23 2	cnmpt2nd	⊢ ( 𝜑 → ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) , 𝑦 ∈ 𝑌 ↦ 𝑦 ) ∈ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) Cn 𝐾 ) )
71	69 70	eqeltrid	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( 2^nd ‘ 𝑤 ) ) ∈ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) Cn 𝐾 ) )
72	33 68 71	cnmpt1t	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) , ( 2^nd ‘ 𝑤 ) ⟩ ) ∈ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) Cn ( 𝐽 ×_t 𝐾 ) ) )
73		fveq2	⊢ ( 𝑢 = ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) , ( 2^nd ‘ 𝑤 ) ⟩ → ( ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ‘ 𝑢 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ‘ ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) , ( 2^nd ‘ 𝑤 ) ⟩ ) )
74		df-ov	⊢ ( ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ( 2^nd ‘ 𝑤 ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ‘ ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) , ( 2^nd ‘ 𝑤 ) ⟩ )
75	73 74	eqtr4di	⊢ ( 𝑢 = ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) , ( 2^nd ‘ 𝑤 ) ⟩ → ( ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ‘ 𝑢 ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ( 2^nd ‘ 𝑤 ) ) )
76	33 8 35 38 59 72 75	cnmptk1p	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) × 𝑌 ) ↦ ( ( 2^nd ‘ ( 1^st ‘ 𝑤 ) ) ( 1^st ‘ ( 1^st ‘ 𝑤 ) ) ( 2^nd ‘ 𝑤 ) ) ) ∈ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) Cn 𝐿 ) )
77	31 76	eqeltrrid	⊢ ( 𝜑 → ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) , 𝑦 ∈ 𝑌 ↦ ( ( 2^nd ‘ 𝑧 ) ( 1^st ‘ 𝑧 ) 𝑦 ) ) ∈ ( ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) ×_t 𝐾 ) Cn 𝐿 ) )
78	23 2 77	cnmpt2k	⊢ ( 𝜑 → ( 𝑧 ∈ ( ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) × 𝑋 ) ↦ ( 𝑦 ∈ 𝑌 ↦ ( ( 2^nd ‘ 𝑧 ) ( 1^st ‘ 𝑧 ) 𝑦 ) ) ) ∈ ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) Cn ( 𝐿 ↑_ko 𝐾 ) ) )
79	21 78	eqeltrrid	⊢ ( 𝜑 → ( 𝑓 ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) , 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ∈ ( ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ×_t 𝐽 ) Cn ( 𝐿 ↑_ko 𝐾 ) ) )
80	13 1 79	cnmpt2k	⊢ ( 𝜑 → ( 𝑓 ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐿 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( 𝑦 ∈ 𝑌 ↦ ( 𝑥 𝑓 𝑦 ) ) ) ) ∈ ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) Cn ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ) )
81	3 80	eqeltrid	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) Cn ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ) )
82	1 2 3 4 5 6	xkocnv	⊢ ( 𝜑 → ^◡ 𝐹 = ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) ) )
83	15 25	op1std	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 1^st ‘ 𝑧 ) = 𝑥 )
84	83	fveq2d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑔 ‘ ( 1^st ‘ 𝑧 ) ) = ( 𝑔 ‘ 𝑥 ) )
85	15 25	op2ndd	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2^nd ‘ 𝑧 ) = 𝑦 )
86	84 85	fveq12d	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑔 ‘ ( 1^st ‘ 𝑧 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) = ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
87	86	mpompt	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 𝑔 ‘ ( 1^st ‘ 𝑧 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) )
88	87	mpteq2i	⊢ ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) ↦ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 𝑔 ‘ ( 1^st ‘ 𝑧 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ) = ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ ( ( 𝑔 ‘ 𝑥 ) ‘ 𝑦 ) ) )
89	82 88	eqtr4di	⊢ ( 𝜑 → ^◡ 𝐹 = ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) ↦ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 𝑔 ‘ ( 1^st ‘ 𝑧 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ) )
90		nllytop	⊢ ( 𝐽 ∈ 𝑛-Locally Comp → 𝐽 ∈ Top )
91	4 90	syl	⊢ ( 𝜑 → 𝐽 ∈ Top )
92		nllytop	⊢ ( 𝐾 ∈ 𝑛-Locally Comp → 𝐾 ∈ Top )
93	5 92	syl	⊢ ( 𝜑 → 𝐾 ∈ Top )
94		xkotop	⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ Top ) → ( 𝐿 ↑_ko 𝐾 ) ∈ Top )
95	93 6 94	syl2anc	⊢ ( 𝜑 → ( 𝐿 ↑_ko 𝐾 ) ∈ Top )
96		eqid	⊢ ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) = ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 )
97	96	xkotopon	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐿 ↑_ko 𝐾 ) ∈ Top ) → ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ∈ ( TopOn ‘ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) ) )
98	91 95 97	syl2anc	⊢ ( 𝜑 → ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ∈ ( TopOn ‘ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) ) )
99		vex	⊢ 𝑔 ∈ V
100	99 24	op1std	⊢ ( 𝑤 = ⟨ 𝑔 , 𝑧 ⟩ → ( 1^st ‘ 𝑤 ) = 𝑔 )
101	99 24	op2ndd	⊢ ( 𝑤 = ⟨ 𝑔 , 𝑧 ⟩ → ( 2^nd ‘ 𝑤 ) = 𝑧 )
102	101	fveq2d	⊢ ( 𝑤 = ⟨ 𝑔 , 𝑧 ⟩ → ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) = ( 1^st ‘ 𝑧 ) )
103	100 102	fveq12d	⊢ ( 𝑤 = ⟨ 𝑔 , 𝑧 ⟩ → ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) = ( 𝑔 ‘ ( 1^st ‘ 𝑧 ) ) )
104	101	fveq2d	⊢ ( 𝑤 = ⟨ 𝑔 , 𝑧 ⟩ → ( 2^nd ‘ ( 2^nd ‘ 𝑤 ) ) = ( 2^nd ‘ 𝑧 ) )
105	103 104	fveq12d	⊢ ( 𝑤 = ⟨ 𝑔 , 𝑧 ⟩ → ( ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑤 ) ) ) = ( ( 𝑔 ‘ ( 1^st ‘ 𝑧 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) )
106	105	mpompt	⊢ ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑤 ) ) ) ) = ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) , 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 𝑔 ‘ ( 1^st ‘ 𝑧 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) )
107		txtopon	⊢ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ∈ ( TopOn ‘ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) ) ∧ ( 𝐽 ×_t 𝐾 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ) → ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) ∈ ( TopOn ‘ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) )
108	98 8 107	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) ∈ ( TopOn ‘ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) )
109	2	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
110	35	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) → 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) )
111		eqid	⊢ ( 𝐿 ↑_ko 𝐾 ) = ( 𝐿 ↑_ko 𝐾 )
112	111	xkotopon	⊢ ( ( 𝐾 ∈ Top ∧ 𝐿 ∈ Top ) → ( 𝐿 ↑_ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
113	93 6 112	syl2anc	⊢ ( 𝜑 → ( 𝐿 ↑_ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) )
114		xp1st	⊢ ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) → ( 1^st ‘ 𝑤 ) ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) )
115		cnf2	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐿 ↑_ko 𝐾 ) ∈ ( TopOn ‘ ( 𝐾 Cn 𝐿 ) ) ∧ ( 1^st ‘ 𝑤 ) ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) ) → ( 1^st ‘ 𝑤 ) : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
116	1 113 114 115	syl2an3an	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) → ( 1^st ‘ 𝑤 ) : 𝑋 ⟶ ( 𝐾 Cn 𝐿 ) )
117		xp2nd	⊢ ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) → ( 2^nd ‘ 𝑤 ) ∈ ( 𝑋 × 𝑌 ) )
118	117	adantl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) → ( 2^nd ‘ 𝑤 ) ∈ ( 𝑋 × 𝑌 ) )
119		xp1st	⊢ ( ( 2^nd ‘ 𝑤 ) ∈ ( 𝑋 × 𝑌 ) → ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ∈ 𝑋 )
120	118 119	syl	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) → ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ∈ 𝑋 )
121	116 120	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) → ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ∈ ( 𝐾 Cn 𝐿 ) )
122		cnf2	⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐿 ∈ ( TopOn ‘ ∪ 𝐿 ) ∧ ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ∈ ( 𝐾 Cn 𝐿 ) ) → ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) : 𝑌 ⟶ ∪ 𝐿 )
123	109 110 121 122	syl3anc	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) → ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) : 𝑌 ⟶ ∪ 𝐿 )
124	123	feqmptd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) → ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ‘ 𝑦 ) ) )
125	124	mpteq2dva	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ) = ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 𝑦 ∈ 𝑌 ↦ ( ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ‘ 𝑦 ) ) ) )
126	100	mpompt	⊢ ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 1^st ‘ 𝑤 ) ) = ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) , 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ 𝑔 )
127	116	feqmptd	⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ) → ( 1^st ‘ 𝑤 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ) )
128	127	mpteq2dva	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 1^st ‘ 𝑤 ) ) = ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ) ) )
129	126 128	eqtr3id	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) , 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ 𝑔 ) = ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ) ) )
130	98 8	cnmpt1st	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) , 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ 𝑔 ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ) )
131	129 130	eqeltrrd	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) ) ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ) )
132	102	mpompt	⊢ ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) = ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) , 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1^st ‘ 𝑧 ) )
133	98 8	cnmpt2nd	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) , 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ 𝑧 ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn ( 𝐽 ×_t 𝐾 ) ) )
134	52	cbvmptv	⊢ ( 𝑡 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1^st ‘ 𝑡 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1^st ‘ 𝑧 ) )
135	83	mpompt	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1^st ‘ 𝑧 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑥 )
136	1 2	cnmpt1st	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑥 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐽 ) )
137	135 136	eqeltrid	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1^st ‘ 𝑧 ) ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐽 ) )
138	134 137	eqeltrid	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1^st ‘ 𝑡 ) ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐽 ) )
139	98 8 133 8 138 52	cnmpt21	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) , 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 1^st ‘ 𝑧 ) ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn 𝐽 ) )
140	132 139	eqeltrid	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn 𝐽 ) )
141		fveq2	⊢ ( 𝑥 = ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) → ( ( 1^st ‘ 𝑤 ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) )
142	108 1 113 4 131 140 141	cnmptk1p	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn ( 𝐿 ↑_ko 𝐾 ) ) )
143	125 142	eqeltrrd	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 𝑦 ∈ 𝑌 ↦ ( ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ‘ 𝑦 ) ) ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn ( 𝐿 ↑_ko 𝐾 ) ) )
144	104	mpompt	⊢ ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 2^nd ‘ ( 2^nd ‘ 𝑤 ) ) ) = ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) , 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2^nd ‘ 𝑧 ) )
145	61	cbvmptv	⊢ ( 𝑡 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2^nd ‘ 𝑡 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2^nd ‘ 𝑧 ) )
146	85	mpompt	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2^nd ‘ 𝑧 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑦 )
147	1 2	cnmpt2nd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑦 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐾 ) )
148	146 147	eqeltrid	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐾 ) )
149	145 148	eqeltrid	⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2^nd ‘ 𝑡 ) ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐾 ) )
150	98 8 133 8 149 61	cnmpt21	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) , 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn 𝐾 ) )
151	144 150	eqeltrid	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( 2^nd ‘ ( 2^nd ‘ 𝑤 ) ) ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn 𝐾 ) )
152		fveq2	⊢ ( 𝑦 = ( 2^nd ‘ ( 2^nd ‘ 𝑤 ) ) → ( ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ‘ 𝑦 ) = ( ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑤 ) ) ) )
153	108 2 35 5 143 151 152	cnmptk1p	⊢ ( 𝜑 → ( 𝑤 ∈ ( ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) × ( 𝑋 × 𝑌 ) ) ↦ ( ( ( 1^st ‘ 𝑤 ) ‘ ( 1^st ‘ ( 2^nd ‘ 𝑤 ) ) ) ‘ ( 2^nd ‘ ( 2^nd ‘ 𝑤 ) ) ) ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn 𝐿 ) )
154	106 153	eqeltrrid	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) , 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 𝑔 ‘ ( 1^st ‘ 𝑧 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ∈ ( ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ×_t ( 𝐽 ×_t 𝐾 ) ) Cn 𝐿 ) )
155	98 8 154	cnmpt2k	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐽 Cn ( 𝐿 ↑_ko 𝐾 ) ) ↦ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 𝑔 ‘ ( 1^st ‘ 𝑧 ) ) ‘ ( 2^nd ‘ 𝑧 ) ) ) ) ∈ ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) Cn ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ) )
156	89 155	eqeltrd	⊢ ( 𝜑 → ^◡ 𝐹 ∈ ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) Cn ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ) )
157		ishmeo	⊢ ( 𝐹 ∈ ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) Homeo ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ) ↔ ( 𝐹 ∈ ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) Cn ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ) ∧ ^◡ 𝐹 ∈ ( ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) Cn ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) ) ) )
158	81 156 157	sylanbrc	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐿 ↑_ko ( 𝐽 ×_t 𝐾 ) ) Homeo ( ( 𝐿 ↑_ko 𝐾 ) ↑_ko 𝐽 ) ) )

Metamath Proof Explorer

Theorem xkohmeo

Proof