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	$⊢ φ \to J \in TopOn (X)$
	xkohmeo.y	$⊢ φ \to K \in TopOn (Y)$
	xkohmeo.f	$⊢ F = (f \in ((J \times_{t} K) Cn L) ⟼ (x \in X ⟼ (y \in Y ⟼ x f y)))$
	xkohmeo.j	$⊢ φ \to J \in N-LocallyComp$
	xkohmeo.k	$⊢ φ \to K \in N-LocallyComp$
	xkohmeo.l	$⊢ φ \to L \in Top$
Assertion	xkohmeo	$⊢ φ \to F \in ((L^_{ko} (J \times_{t} K)) Homeo ((L^_{ko} K)^_{ko} J))$

Proof

Step	Hyp	Ref	Expression
1		xkohmeo.x	$⊢ φ \to J \in TopOn (X)$
2		xkohmeo.y	$⊢ φ \to K \in TopOn (Y)$
3		xkohmeo.f	$⊢ F = (f \in ((J \times_{t} K) Cn L) ⟼ (x \in X ⟼ (y \in Y ⟼ x f y)))$
4		xkohmeo.j	$⊢ φ \to J \in N-LocallyComp$
5		xkohmeo.k	$⊢ φ \to K \in N-LocallyComp$
6		xkohmeo.l	$⊢ φ \to L \in Top$
7		txtopon	$⊢ (J \in TopOn (X) \land K \in TopOn (Y)) \to J \times_{t} K \in TopOn (X \times Y)$
8	1 2 7	syl2anc	$⊢ φ \to J \times_{t} K \in TopOn (X \times Y)$
9		topontop	$⊢ J \times_{t} K \in TopOn (X \times Y) \to J \times_{t} K \in Top$
10	8 9	syl	$⊢ φ \to J \times_{t} K \in Top$
11		eqid	$⊢ L^_{ko} (J \times_{t} K) = L^_{ko} (J \times_{t} K)$
12	11	xkotopon	$⊢ (J \times_{t} K \in Top \land L \in Top) \to L^_{ko} (J \times_{t} K) \in TopOn ((J \times_{t} K) Cn L)$
13	10 6 12	syl2anc	$⊢ φ \to L^_{ko} (J \times_{t} K) \in TopOn ((J \times_{t} K) Cn L)$
14		vex	$⊢ f \in V$
15		vex	$⊢ x \in V$
16	14 15	op1std	$⊢ z = ⟨f, x⟩ \to 1^{st} (z) = f$
17	14 15	op2ndd	$⊢ z = ⟨f, x⟩ \to 2^{nd} (z) = x$
18		eqidd	$⊢ z = ⟨f, x⟩ \to y = y$
19	16 17 18	oveq123d	$⊢ z = ⟨f, x⟩ \to 2^{nd} (z) 1^{st} (z) y = x f y$
20	19	mpteq2dv	$⊢ z = ⟨f, x⟩ \to (y \in Y ⟼ 2^{nd} (z) 1^{st} (z) y) = (y \in Y ⟼ x f y)$
21	20	mpompt	$⊢ (z \in (((J \times_{t} K) Cn L) \times X) ⟼ (y \in Y ⟼ 2^{nd} (z) 1^{st} (z) y)) = (f \in ((J \times_{t} K) Cn L), x \in X ⟼ (y \in Y ⟼ x f y))$
22		txtopon	$⊢ (L^_{ko} (J \times_{t} K) \in TopOn ((J \times_{t} K) Cn L) \land J \in TopOn (X)) \to (L^_{ko} (J \times_{t} K)) \times_{t} J \in TopOn (((J \times_{t} K) Cn L) \times X)$
23	13 1 22	syl2anc	$⊢ φ \to (L^_{ko} (J \times_{t} K)) \times_{t} J \in TopOn (((J \times_{t} K) Cn L) \times X)$
24		vex	$⊢ z \in V$
25		vex	$⊢ y \in V$
26	24 25	op1std	$⊢ w = ⟨z, y⟩ \to 1^{st} (w) = z$
27	26	fveq2d	$⊢ w = ⟨z, y⟩ \to 1^{st} (1^{st} (w)) = 1^{st} (z)$
28	26	fveq2d	$⊢ w = ⟨z, y⟩ \to 2^{nd} (1^{st} (w)) = 2^{nd} (z)$
29	24 25	op2ndd	$⊢ w = ⟨z, y⟩ \to 2^{nd} (w) = y$
30	27 28 29	oveq123d	$⊢ w = ⟨z, y⟩ \to 2^{nd} (1^{st} (w)) 1^{st} (1^{st} (w)) 2^{nd} (w) = 2^{nd} (z) 1^{st} (z) y$
31	30	mpompt	$⊢ (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ 2^{nd} (1^{st} (w)) 1^{st} (1^{st} (w)) 2^{nd} (w)) = (z \in (((J \times_{t} K) Cn L) \times X), y \in Y ⟼ 2^{nd} (z) 1^{st} (z) y)$
32		txtopon	$⊢ ((L^_{ko} (J \times_{t} K)) \times_{t} J \in TopOn (((J \times_{t} K) Cn L) \times X) \land K \in TopOn (Y)) \to ((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K \in TopOn ((((J \times_{t} K) Cn L) \times X) \times Y)$
33	23 2 32	syl2anc	$⊢ φ \to ((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K \in TopOn ((((J \times_{t} K) Cn L) \times X) \times Y)$
34		toptopon2	$⊢ L \in Top \leftrightarrow L \in TopOn (⋃ L)$
35	6 34	sylib	$⊢ φ \to L \in TopOn (⋃ L)$
36		txcmp	$⊢ (x \in Comp \land y \in Comp) \to x \times_{t} y \in Comp$
37	36	txnlly	$⊢ (J \in N-LocallyComp\landK \in N-LocallyComp\toJ \times_{t} K \in N-LocallyComp)$
38	4 5 37	syl2anc	$⊢ φ \to J \times_{t} K \in N-LocallyComp$
39	27	mpompt	$⊢ (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ 1^{st} (1^{st} (w))) = (z \in (((J \times_{t} K) Cn L) \times X), y \in Y ⟼ 1^{st} (z))$
40	8	adantr	$⊢ (φ \land w \in ((((J \times_{t} K) Cn L) \times X) \times Y)) \to J \times_{t} K \in TopOn (X \times Y)$
41	35	adantr	$⊢ (φ \land w \in ((((J \times_{t} K) Cn L) \times X) \times Y)) \to L \in TopOn (⋃ L)$
42		xp1st	$⊢ w \in ((((J \times_{t} K) Cn L) \times X) \times Y) \to 1^{st} (w) \in (((J \times_{t} K) Cn L) \times X)$
43	42	adantl	$⊢ (φ \land w \in ((((J \times_{t} K) Cn L) \times X) \times Y)) \to 1^{st} (w) \in (((J \times_{t} K) Cn L) \times X)$
44		xp1st	$⊢ 1^{st} (w) \in (((J \times_{t} K) Cn L) \times X) \to 1^{st} (1^{st} (w)) \in ((J \times_{t} K) Cn L)$
45	43 44	syl	$⊢ (φ \land w \in ((((J \times_{t} K) Cn L) \times X) \times Y)) \to 1^{st} (1^{st} (w)) \in ((J \times_{t} K) Cn L)$
46		cnf2	$⊢ (J \times_{t} K \in TopOn (X \times Y) \land L \in TopOn (⋃ L) \land 1^{st} (1^{st} (w)) \in ((J \times_{t} K) Cn L)) \to 1^{st} (1^{st} (w)) : X \times Y ⟶ ⋃ L$
47	40 41 45 46	syl3anc	$⊢ (φ \land w \in ((((J \times_{t} K) Cn L) \times X) \times Y)) \to 1^{st} (1^{st} (w)) : X \times Y ⟶ ⋃ L$
48	47	feqmptd	$⊢ (φ \land w \in ((((J \times_{t} K) Cn L) \times X) \times Y)) \to 1^{st} (1^{st} (w)) = (u \in (X \times Y) ⟼ 1^{st} (1^{st} (w)) (u))$
49	48	mpteq2dva	$⊢ φ \to (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ 1^{st} (1^{st} (w))) = (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ (u \in (X \times Y) ⟼ 1^{st} (1^{st} (w)) (u)))$
50	39 49	syl5eqr	$⊢ φ \to (z \in (((J \times_{t} K) Cn L) \times X), y \in Y ⟼ 1^{st} (z)) = (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ (u \in (X \times Y) ⟼ 1^{st} (1^{st} (w)) (u)))$
51	23 2	cnmpt1st	$⊢ φ \to (z \in (((J \times_{t} K) Cn L) \times X), y \in Y ⟼ z) \in ((((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K) Cn ((L^_{ko} (J \times_{t} K)) \times_{t} J))$
52		fveq2	$⊢ t = z \to 1^{st} (t) = 1^{st} (z)$
53	52	cbvmptv	$⊢ (t \in (((J \times_{t} K) Cn L) \times X) ⟼ 1^{st} (t)) = (z \in (((J \times_{t} K) Cn L) \times X) ⟼ 1^{st} (z))$
54	16	mpompt	$⊢ (z \in (((J \times_{t} K) Cn L) \times X) ⟼ 1^{st} (z)) = (f \in ((J \times_{t} K) Cn L), x \in X ⟼ f)$
55	13 1	cnmpt1st	$⊢ φ \to (f \in ((J \times_{t} K) Cn L), x \in X ⟼ f) \in (((L^_{ko} (J \times_{t} K)) \times_{t} J) Cn (L^_{ko} (J \times_{t} K)))$
56	54 55	eqeltrid	$⊢ φ \to (z \in (((J \times_{t} K) Cn L) \times X) ⟼ 1^{st} (z)) \in (((L^_{ko} (J \times_{t} K)) \times_{t} J) Cn (L^_{ko} (J \times_{t} K)))$
57	53 56	eqeltrid	$⊢ φ \to (t \in (((J \times_{t} K) Cn L) \times X) ⟼ 1^{st} (t)) \in (((L^_{ko} (J \times_{t} K)) \times_{t} J) Cn (L^_{ko} (J \times_{t} K)))$
58	23 2 51 23 57 52	cnmpt21	$⊢ φ \to (z \in (((J \times_{t} K) Cn L) \times X), y \in Y ⟼ 1^{st} (z)) \in ((((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K) Cn (L^_{ko} (J \times_{t} K)))$
59	50 58	eqeltrrd	$⊢ φ \to (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ (u \in (X \times Y) ⟼ 1^{st} (1^{st} (w)) (u))) \in ((((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K) Cn (L^_{ko} (J \times_{t} K)))$
60	28	mpompt	$⊢ (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ 2^{nd} (1^{st} (w))) = (z \in (((J \times_{t} K) Cn L) \times X), y \in Y ⟼ 2^{nd} (z))$
61		fveq2	$⊢ t = z \to 2^{nd} (t) = 2^{nd} (z)$
62	61	cbvmptv	$⊢ (t \in (((J \times_{t} K) Cn L) \times X) ⟼ 2^{nd} (t)) = (z \in (((J \times_{t} K) Cn L) \times X) ⟼ 2^{nd} (z))$
63	17	mpompt	$⊢ (z \in (((J \times_{t} K) Cn L) \times X) ⟼ 2^{nd} (z)) = (f \in ((J \times_{t} K) Cn L), x \in X ⟼ x)$
64	13 1	cnmpt2nd	$⊢ φ \to (f \in ((J \times_{t} K) Cn L), x \in X ⟼ x) \in (((L^_{ko} (J \times_{t} K)) \times_{t} J) Cn J)$
65	63 64	eqeltrid	$⊢ φ \to (z \in (((J \times_{t} K) Cn L) \times X) ⟼ 2^{nd} (z)) \in (((L^_{ko} (J \times_{t} K)) \times_{t} J) Cn J)$
66	62 65	eqeltrid	$⊢ φ \to (t \in (((J \times_{t} K) Cn L) \times X) ⟼ 2^{nd} (t)) \in (((L^_{ko} (J \times_{t} K)) \times_{t} J) Cn J)$
67	23 2 51 23 66 61	cnmpt21	$⊢ φ \to (z \in (((J \times_{t} K) Cn L) \times X), y \in Y ⟼ 2^{nd} (z)) \in ((((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K) Cn J)$
68	60 67	eqeltrid	$⊢ φ \to (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ 2^{nd} (1^{st} (w))) \in ((((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K) Cn J)$
69	29	mpompt	$⊢ (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ 2^{nd} (w)) = (z \in (((J \times_{t} K) Cn L) \times X), y \in Y ⟼ y)$
70	23 2	cnmpt2nd	$⊢ φ \to (z \in (((J \times_{t} K) Cn L) \times X), y \in Y ⟼ y) \in ((((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K) Cn K)$
71	69 70	eqeltrid	$⊢ φ \to (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ 2^{nd} (w)) \in ((((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K) Cn K)$
72	33 68 71	cnmpt1t	$⊢ φ \to (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ ⟨2^{nd} (1^{st} (w)), 2^{nd} (w)⟩) \in ((((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K) Cn (J \times_{t} K))$
73		fveq2	$⊢ u = ⟨2^{nd} (1^{st} (w)), 2^{nd} (w)⟩ \to 1^{st} (1^{st} (w)) (u) = 1^{st} (1^{st} (w)) (⟨2^{nd} (1^{st} (w)), 2^{nd} (w)⟩)$
74		df-ov	$⊢ 2^{nd} (1^{st} (w)) 1^{st} (1^{st} (w)) 2^{nd} (w) = 1^{st} (1^{st} (w)) (⟨2^{nd} (1^{st} (w)), 2^{nd} (w)⟩)$
75	73 74	syl6eqr	$⊢ u = ⟨2^{nd} (1^{st} (w)), 2^{nd} (w)⟩ \to 1^{st} (1^{st} (w)) (u) = 2^{nd} (1^{st} (w)) 1^{st} (1^{st} (w)) 2^{nd} (w)$
76	33 8 35 38 59 72 75	cnmptk1p	$⊢ φ \to (w \in ((((J \times_{t} K) Cn L) \times X) \times Y) ⟼ 2^{nd} (1^{st} (w)) 1^{st} (1^{st} (w)) 2^{nd} (w)) \in ((((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K) Cn L)$
77	31 76	eqeltrrid	$⊢ φ \to (z \in (((J \times_{t} K) Cn L) \times X), y \in Y ⟼ 2^{nd} (z) 1^{st} (z) y) \in ((((L^_{ko} (J \times_{t} K)) \times_{t} J) \times_{t} K) Cn L)$
78	23 2 77	cnmpt2k	$⊢ φ \to (z \in (((J \times_{t} K) Cn L) \times X) ⟼ (y \in Y ⟼ 2^{nd} (z) 1^{st} (z) y)) \in (((L^_{ko} (J \times_{t} K)) \times_{t} J) Cn (L^_{ko} K))$
79	21 78	eqeltrrid	$⊢ φ \to (f \in ((J \times_{t} K) Cn L), x \in X ⟼ (y \in Y ⟼ x f y)) \in (((L^_{ko} (J \times_{t} K)) \times_{t} J) Cn (L^_{ko} K))$
80	13 1 79	cnmpt2k	$⊢ φ \to (f \in ((J \times_{t} K) Cn L) ⟼ (x \in X ⟼ (y \in Y ⟼ x f y))) \in ((L^_{ko} (J \times_{t} K)) Cn ((L^_{ko} K)^_{ko} J))$
81	3 80	eqeltrid	$⊢ φ \to F \in ((L^_{ko} (J \times_{t} K)) Cn ((L^_{ko} K)^_{ko} J))$
82	1 2 3 4 5 6	xkocnv	$⊢ φ \to F^{-1} = (g \in (J Cn (L^_{ko} K)) ⟼ (x \in X, y \in Y ⟼ g (x) (y)))$
83	15 25	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
84	83	fveq2d	$⊢ z = ⟨x, y⟩ \to g (1^{st} (z)) = g (x)$
85	15 25	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
86	84 85	fveq12d	$⊢ z = ⟨x, y⟩ \to g (1^{st} (z)) (2^{nd} (z)) = g (x) (y)$
87	86	mpompt	$⊢ (z \in (X \times Y) ⟼ g (1^{st} (z)) (2^{nd} (z))) = (x \in X, y \in Y ⟼ g (x) (y))$
88	87	mpteq2i	$⊢ (g \in (J Cn (L^_{ko} K)) ⟼ (z \in (X \times Y) ⟼ g (1^{st} (z)) (2^{nd} (z)))) = (g \in (J Cn (L^_{ko} K)) ⟼ (x \in X, y \in Y ⟼ g (x) (y)))$
89	82 88	syl6eqr	$⊢ φ \to F^{-1} = (g \in (J Cn (L^_{ko} K)) ⟼ (z \in (X \times Y) ⟼ g (1^{st} (z)) (2^{nd} (z))))$
90		nllytop	$⊢ J \in N-LocallyComp\toJ \in Top$
91	4 90	syl	$⊢ φ \to J \in Top$
92		nllytop	$⊢ K \in N-LocallyComp\toK \in Top$
93	5 92	syl	$⊢ φ \to K \in Top$
94		xkotop	$⊢ (K \in Top \land L \in Top) \to L^_{ko} K \in Top$
95	93 6 94	syl2anc	$⊢ φ \to L^_{ko} K \in Top$
96		eqid	$⊢ (L^_{ko} K)^_{ko} J = (L^_{ko} K)^_{ko} J$
97	96	xkotopon	$⊢ (J \in Top \land L^_{ko} K \in Top) \to (L^_{ko} K)^_{ko} J \in TopOn (J Cn (L^_{ko} K))$
98	91 95 97	syl2anc	$⊢ φ \to (L^_{ko} K)^_{ko} J \in TopOn (J Cn (L^_{ko} K))$
99		vex	$⊢ g \in V$
100	99 24	op1std	$⊢ w = ⟨g, z⟩ \to 1^{st} (w) = g$
101	99 24	op2ndd	$⊢ w = ⟨g, z⟩ \to 2^{nd} (w) = z$
102	101	fveq2d	$⊢ w = ⟨g, z⟩ \to 1^{st} (2^{nd} (w)) = 1^{st} (z)$
103	100 102	fveq12d	$⊢ w = ⟨g, z⟩ \to 1^{st} (w) (1^{st} (2^{nd} (w))) = g (1^{st} (z))$
104	101	fveq2d	$⊢ w = ⟨g, z⟩ \to 2^{nd} (2^{nd} (w)) = 2^{nd} (z)$
105	103 104	fveq12d	$⊢ w = ⟨g, z⟩ \to 1^{st} (w) (1^{st} (2^{nd} (w))) (2^{nd} (2^{nd} (w))) = g (1^{st} (z)) (2^{nd} (z))$
106	105	mpompt	$⊢ (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ 1^{st} (w) (1^{st} (2^{nd} (w))) (2^{nd} (2^{nd} (w)))) = (g \in (J Cn (L^_{ko} K)), z \in (X \times Y) ⟼ g (1^{st} (z)) (2^{nd} (z)))$
107		txtopon	$⊢ ((L^_{ko} K)^_{ko} J \in TopOn (J Cn (L^_{ko} K)) \land J \times_{t} K \in TopOn (X \times Y)) \to ((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K) \in TopOn ((J Cn (L^_{ko} K)) \times (X \times Y))$
108	98 8 107	syl2anc	$⊢ φ \to ((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K) \in TopOn ((J Cn (L^_{ko} K)) \times (X \times Y))$
109	2	adantr	$⊢ (φ \land w \in ((J Cn (L^_{ko} K)) \times (X \times Y))) \to K \in TopOn (Y)$
110	35	adantr	$⊢ (φ \land w \in ((J Cn (L^_{ko} K)) \times (X \times Y))) \to L \in TopOn (⋃ L)$
111		eqid	$⊢ L^_{ko} K = L^_{ko} K$
112	111	xkotopon	$⊢ (K \in Top \land L \in Top) \to L^_{ko} K \in TopOn (K Cn L)$
113	93 6 112	syl2anc	$⊢ φ \to L^_{ko} K \in TopOn (K Cn L)$
114		xp1st	$⊢ w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) \to 1^{st} (w) \in (J Cn (L^_{ko} K))$
115		cnf2	$⊢ (J \in TopOn (X) \land L^_{ko} K \in TopOn (K Cn L) \land 1^{st} (w) \in (J Cn (L^_{ko} K))) \to 1^{st} (w) : X ⟶ K Cn L$
116	1 113 114 115	syl2an3an	$⊢ (φ \land w \in ((J Cn (L^_{ko} K)) \times (X \times Y))) \to 1^{st} (w) : X ⟶ K Cn L$
117		xp2nd	$⊢ w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) \to 2^{nd} (w) \in (X \times Y)$
118	117	adantl	$⊢ (φ \land w \in ((J Cn (L^_{ko} K)) \times (X \times Y))) \to 2^{nd} (w) \in (X \times Y)$
119		xp1st	$⊢ 2^{nd} (w) \in (X \times Y) \to 1^{st} (2^{nd} (w)) \in X$
120	118 119	syl	$⊢ (φ \land w \in ((J Cn (L^_{ko} K)) \times (X \times Y))) \to 1^{st} (2^{nd} (w)) \in X$
121	116 120	ffvelrnd	$⊢ (φ \land w \in ((J Cn (L^_{ko} K)) \times (X \times Y))) \to 1^{st} (w) (1^{st} (2^{nd} (w))) \in (K Cn L)$
122		cnf2	$⊢ (K \in TopOn (Y) \land L \in TopOn (⋃ L) \land 1^{st} (w) (1^{st} (2^{nd} (w))) \in (K Cn L)) \to 1^{st} (w) (1^{st} (2^{nd} (w))) : Y ⟶ ⋃ L$
123	109 110 121 122	syl3anc	$⊢ (φ \land w \in ((J Cn (L^_{ko} K)) \times (X \times Y))) \to 1^{st} (w) (1^{st} (2^{nd} (w))) : Y ⟶ ⋃ L$
124	123	feqmptd	$⊢ (φ \land w \in ((J Cn (L^_{ko} K)) \times (X \times Y))) \to 1^{st} (w) (1^{st} (2^{nd} (w))) = (y \in Y ⟼ 1^{st} (w) (1^{st} (2^{nd} (w))) (y))$
125	124	mpteq2dva	$⊢ φ \to (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ 1^{st} (w) (1^{st} (2^{nd} (w)))) = (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ (y \in Y ⟼ 1^{st} (w) (1^{st} (2^{nd} (w))) (y)))$
126	100	mpompt	$⊢ (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ 1^{st} (w)) = (g \in (J Cn (L^_{ko} K)), z \in (X \times Y) ⟼ g)$
127	116	feqmptd	$⊢ (φ \land w \in ((J Cn (L^_{ko} K)) \times (X \times Y))) \to 1^{st} (w) = (x \in X ⟼ 1^{st} (w) (x))$
128	127	mpteq2dva	$⊢ φ \to (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ 1^{st} (w)) = (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ (x \in X ⟼ 1^{st} (w) (x)))$
129	126 128	syl5eqr	$⊢ φ \to (g \in (J Cn (L^_{ko} K)), z \in (X \times Y) ⟼ g) = (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ (x \in X ⟼ 1^{st} (w) (x)))$
130	98 8	cnmpt1st	$⊢ φ \to (g \in (J Cn (L^_{ko} K)), z \in (X \times Y) ⟼ g) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn ((L^_{ko} K)^_{ko} J))$
131	129 130	eqeltrrd	$⊢ φ \to (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ (x \in X ⟼ 1^{st} (w) (x))) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn ((L^_{ko} K)^_{ko} J))$
132	102	mpompt	$⊢ (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ 1^{st} (2^{nd} (w))) = (g \in (J Cn (L^_{ko} K)), z \in (X \times Y) ⟼ 1^{st} (z))$
133	98 8	cnmpt2nd	$⊢ φ \to (g \in (J Cn (L^_{ko} K)), z \in (X \times Y) ⟼ z) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn (J \times_{t} K))$
134	52	cbvmptv	$⊢ (t \in (X \times Y) ⟼ 1^{st} (t)) = (z \in (X \times Y) ⟼ 1^{st} (z))$
135	83	mpompt	$⊢ (z \in (X \times Y) ⟼ 1^{st} (z)) = (x \in X, y \in Y ⟼ x)$
136	1 2	cnmpt1st	$⊢ φ \to (x \in X, y \in Y ⟼ x) \in ((J \times_{t} K) Cn J)$
137	135 136	eqeltrid	$⊢ φ \to (z \in (X \times Y) ⟼ 1^{st} (z)) \in ((J \times_{t} K) Cn J)$
138	134 137	eqeltrid	$⊢ φ \to (t \in (X \times Y) ⟼ 1^{st} (t)) \in ((J \times_{t} K) Cn J)$
139	98 8 133 8 138 52	cnmpt21	$⊢ φ \to (g \in (J Cn (L^_{ko} K)), z \in (X \times Y) ⟼ 1^{st} (z)) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn J)$
140	132 139	eqeltrid	$⊢ φ \to (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ 1^{st} (2^{nd} (w))) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn J)$
141		fveq2	$⊢ x = 1^{st} (2^{nd} (w)) \to 1^{st} (w) (x) = 1^{st} (w) (1^{st} (2^{nd} (w)))$
142	108 1 113 4 131 140 141	cnmptk1p	$⊢ φ \to (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ 1^{st} (w) (1^{st} (2^{nd} (w)))) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn (L^_{ko} K))$
143	125 142	eqeltrrd	$⊢ φ \to (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ (y \in Y ⟼ 1^{st} (w) (1^{st} (2^{nd} (w))) (y))) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn (L^_{ko} K))$
144	104	mpompt	$⊢ (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ 2^{nd} (2^{nd} (w))) = (g \in (J Cn (L^_{ko} K)), z \in (X \times Y) ⟼ 2^{nd} (z))$
145	61	cbvmptv	$⊢ (t \in (X \times Y) ⟼ 2^{nd} (t)) = (z \in (X \times Y) ⟼ 2^{nd} (z))$
146	85	mpompt	$⊢ (z \in (X \times Y) ⟼ 2^{nd} (z)) = (x \in X, y \in Y ⟼ y)$
147	1 2	cnmpt2nd	$⊢ φ \to (x \in X, y \in Y ⟼ y) \in ((J \times_{t} K) Cn K)$
148	146 147	eqeltrid	$⊢ φ \to (z \in (X \times Y) ⟼ 2^{nd} (z)) \in ((J \times_{t} K) Cn K)$
149	145 148	eqeltrid	$⊢ φ \to (t \in (X \times Y) ⟼ 2^{nd} (t)) \in ((J \times_{t} K) Cn K)$
150	98 8 133 8 149 61	cnmpt21	$⊢ φ \to (g \in (J Cn (L^_{ko} K)), z \in (X \times Y) ⟼ 2^{nd} (z)) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn K)$
151	144 150	eqeltrid	$⊢ φ \to (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ 2^{nd} (2^{nd} (w))) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn K)$
152		fveq2	$⊢ y = 2^{nd} (2^{nd} (w)) \to 1^{st} (w) (1^{st} (2^{nd} (w))) (y) = 1^{st} (w) (1^{st} (2^{nd} (w))) (2^{nd} (2^{nd} (w)))$
153	108 2 35 5 143 151 152	cnmptk1p	$⊢ φ \to (w \in ((J Cn (L^_{ko} K)) \times (X \times Y)) ⟼ 1^{st} (w) (1^{st} (2^{nd} (w))) (2^{nd} (2^{nd} (w)))) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn L)$
154	106 153	eqeltrrid	$⊢ φ \to (g \in (J Cn (L^_{ko} K)), z \in (X \times Y) ⟼ g (1^{st} (z)) (2^{nd} (z))) \in ((((L^_{ko} K)^_{ko} J) \times_{t} (J \times_{t} K)) Cn L)$
155	98 8 154	cnmpt2k	$⊢ φ \to (g \in (J Cn (L^_{ko} K)) ⟼ (z \in (X \times Y) ⟼ g (1^{st} (z)) (2^{nd} (z)))) \in (((L^_{ko} K)^_{ko} J) Cn (L^_{ko} (J \times_{t} K)))$
156	89 155	eqeltrd	$⊢ φ \to F^{-1} \in (((L^_{ko} K)^_{ko} J) Cn (L^_{ko} (J \times_{t} K)))$
157		ishmeo	$⊢ F \in ((L^_{ko} (J \times_{t} K)) Homeo ((L^_{ko} K)^_{ko} J)) \leftrightarrow (F \in ((L^_{ko} (J \times_{t} K)) Cn ((L^_{ko} K)^_{ko} J)) \land F^{-1} \in (((L^_{ko} K)^_{ko} J) Cn (L^_{ko} (J \times_{t} K))))$
158	81 156 157	sylanbrc	$⊢ φ \to F \in ((L^_{ko} (J \times_{t} K)) Homeo ((L^_{ko} K)^_{ko} J))$

Metamath Proof Explorer

Theorem xkohmeo

Proof