Theorem pt1hmeo 20039

Description: The canonical homeomorphism from a topological product on a singleton to the topology of the factor. (Contributed by Mario Carneiro, 3-Feb-2015.)

Hypotheses

Ref	Expression
pt1hmeo.j	|- K = ( Xt_ ` { <. A , J >. } )
pt1hmeo.a	|- ( ph -> A e. V )
pt1hmeo.r	|- ( ph -> J e. (TopOn ` X ) )

Assertion

Ref	Expression
pt1hmeo	|- ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Homeo K ) )

Distinct variable groups:   x, A   x, J   x, K   ph, x   x, X

Allowed substitution hint:   V( x)

Proof of Theorem pt1hmeo

Dummy variables k y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fconstmpt 5042	. . . . 5 |- ( { A } X. { x } ) = ( k e. { A } |-> x )
2		pt1hmeo.a	. . . . . . 7 |- ( ph -> A e. V )
3	2	adantr 465	. . . . . 6 |- ( ( ph /\ x e. X ) -> A e. V )
4		sneq 4037	. . . . . . . . 9 |- ( k = A -> { k } = { A } )
5	4	xpeq1d 5022	. . . . . . . 8 |- ( k = A -> ( { k } X. { x } ) = ( { A } X. { x } ) )
6		opeq1 4213	. . . . . . . . 9 |- ( k = A -> <. k , x >. = <. A , x >. )
7	6	sneqd 4039	. . . . . . . 8 |- ( k = A -> { <. k , x >. } = { <. A , x >. } )
8	5, 7	eqeq12d 2489	. . . . . . 7 |- ( k = A -> ( ( { k } X. { x } ) = { <. k , x >. } <-> ( { A } X. { x } ) = { <. A , x >. } ) )
9		vex 3116	. . . . . . . 8 |- k e. _V
10		vex 3116	. . . . . . . 8 |- x e. _V
11	9, 10	xpsn 6061	. . . . . . 7 |- ( { k } X. { x } ) = { <. k , x >. }
12	8, 11	vtoclg 3171	. . . . . 6 |- ( A e. V -> ( { A } X. { x } ) = { <. A , x >. } )
13	3, 12	syl 16	. . . . 5 |- ( ( ph /\ x e. X ) -> ( { A } X. { x } ) = { <. A , x >. } )
14	1, 13	syl5eqr 2522	. . . 4 |- ( ( ph /\ x e. X ) -> ( k e. { A } |-> x ) = { <. A , x >. } )
15	14	mpteq2dva 4533	. . 3 |- ( ph -> ( x e. X |-> ( k e. { A } |-> x ) ) = ( x e. X |-> { <. A , x >. } ) )
16		pt1hmeo.j	. . . 4 |- K = ( Xt_ ` { <. A , J >. } )
17		pt1hmeo.r	. . . 4 |- ( ph -> J e. (TopOn ` X ) )
18		snex 4688	. . . . 5 |- { A } e. _V
19	18	a1i 11	. . . 4 |- ( ph -> { A } e. _V )
20		f1osng 5852	. . . . . . 7 |- ( ( A e. V /\ J e. (TopOn ` X ) ) -> { <. A , J >. } : { A } -1-1-onto-> { J } )
21	2, 17, 20	syl2anc 661	. . . . . 6 |- ( ph -> { <. A , J >. } : { A } -1-1-onto-> { J } )
22		f1of 5814	. . . . . 6 |- ( { <. A , J >. } : { A } -1-1-onto-> { J } -> { <. A , J >. } : { A } --> { J } )
23	21, 22	syl 16	. . . . 5 |- ( ph -> { <. A , J >. } : { A } --> { J } )
24		topontop 19191	. . . . . . 7 |- ( J e. (TopOn ` X ) -> J e. Top )
25	17, 24	syl 16	. . . . . 6 |- ( ph -> J e. Top )
26	25	snssd 4172	. . . . 5 |- ( ph -> { J } C_ Top )
27		fss 5737	. . . . 5 |- ( ( { <. A , J >. } : { A } --> { J } /\ { J } C_ Top ) -> { <. A , J >. } : { A } --> Top )
28	23, 26, 27	syl2anc 661	. . . 4 |- ( ph -> { <. A , J >. } : { A } --> Top )
29	17	cnmptid 19894	. . . . . 6 |- ( ph -> ( x e. X |-> x ) e. ( J Cn J ) )
30	29	adantr 465	. . . . 5 |- ( ( ph /\ k e. { A } ) -> ( x e. X |-> x ) e. ( J Cn J ) )
31		elsni 4052	. . . . . . . 8 |- ( k e. { A } -> k = A )
32	31	fveq2d 5868	. . . . . . 7 |- ( k e. { A } -> ( { <. A , J >. } ` k ) = ( { <. A , J >. } ` A ) )
33		fvsng 6093	. . . . . . . 8 |- ( ( A e. V /\ J e. (TopOn ` X ) ) -> ( { <. A , J >. } ` A ) = J )
34	2, 17, 33	syl2anc 661	. . . . . . 7 |- ( ph -> ( { <. A , J >. } ` A ) = J )
35	32, 34	sylan9eqr 2530	. . . . . 6 |- ( ( ph /\ k e. { A } ) -> ( { <. A , J >. } ` k ) = J )
36	35	oveq2d 6298	. . . . 5 |- ( ( ph /\ k e. { A } ) -> ( J Cn ( { <. A , J >. } ` k ) ) = ( J Cn J ) )
37	30, 36	eleqtrrd 2558	. . . 4 |- ( ( ph /\ k e. { A } ) -> ( x e. X |-> x ) e. ( J Cn ( { <. A , J >. } ` k ) ) )
38	16, 17, 19, 28, 37	ptcn 19860	. . 3 |- ( ph -> ( x e. X |-> ( k e. { A } |-> x ) ) e. ( J Cn K ) )
39	15, 38	eqeltrrd 2556	. 2 |- ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Cn K ) )
40		simprr 756	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y = { <. A , x >. } )
41	14	adantrr 716	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) = { <. A , x >. } )
42	40, 41	eqtr4d 2511	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y = ( k e. { A } |-> x ) )
43		simprl 755	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> x e. X )
44	43	adantr 465	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) /\ k e. { A } ) -> x e. X )
45		eqid 2467	. . . . . . . . . . 11 |- ( k e. { A } |-> x ) = ( k e. { A } |-> x )
46	44, 45	fmptd 6043	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) : { A } --> X )
47		toponmax 19193	. . . . . . . . . . . . 13 |- ( J e. (TopOn ` X ) -> X e. J )
48	17, 47	syl 16	. . . . . . . . . . . 12 |- ( ph -> X e. J )
49	48	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> X e. J )
50		elmapg 7430	. . . . . . . . . . 11 |- ( ( X e. J /\ { A } e. _V ) -> ( ( k e. { A } |-> x ) e. ( X ^m { A } ) <-> ( k e. { A } |-> x ) : { A } --> X ) )
51	49, 18, 50	sylancl 662	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( ( k e. { A } |-> x ) e. ( X ^m { A } ) <-> ( k e. { A } |-> x ) : { A } --> X ) )
52	46, 51	mpbird 232	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) e. ( X ^m { A } ) )
53	42, 52	eqeltrd 2555	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y e. ( X ^m { A } ) )
54	40	fveq1d 5866	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( y ` A ) = ( { <. A , x >. } ` A ) )
55	2	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> A e. V )
56		fvsng 6093	. . . . . . . . . 10 |- ( ( A e. V /\ x e. X ) -> ( { <. A , x >. } ` A ) = x )
57	55, 43, 56	syl2anc 661	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( { <. A , x >. } ` A ) = x )
58	54, 57	eqtr2d 2509	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> x = ( y ` A ) )
59	53, 58	jca 532	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) )
60		simprr 756	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> x = ( y ` A ) )
61		simprl 755	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y e. ( X ^m { A } ) )
62	48	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> X e. J )
63		elmapg 7430	. . . . . . . . . . . 12 |- ( ( X e. J /\ { A } e. _V ) -> ( y e. ( X ^m { A } ) <-> y : { A } --> X ) )
64	62, 18, 63	sylancl 662	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y e. ( X ^m { A } ) <-> y : { A } --> X ) )
65	61, 64	mpbid 210	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y : { A } --> X )
66		snidg 4053	. . . . . . . . . . . 12 |- ( A e. V -> A e. { A } )
67	2, 66	syl 16	. . . . . . . . . . 11 |- ( ph -> A e. { A } )
68	67	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> A e. { A } )
69	65, 68	ffvelrnd 6020	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y ` A ) e. X )
70	60, 69	eqeltrd 2555	. . . . . . . 8 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> x e. X )
71	2	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> A e. V )
72	4	feq2d 5716	. . . . . . . . . . . . 13 |- ( k = A -> ( y : { k } --> X <-> y : { A } --> X ) )
73		fveq2 5864	. . . . . . . . . . . . . . 15 |- ( k = A -> ( y ` k ) = ( y ` A ) )
74	73	eleq1d 2536	. . . . . . . . . . . . . 14 |- ( k = A -> ( ( y ` k ) e. X <-> ( y ` A ) e. X ) )
75		id 22	. . . . . . . . . . . . . . . . 17 |- ( k = A -> k = A )
76	75, 73	opeq12d 4221	. . . . . . . . . . . . . . . 16 |- ( k = A -> <. k , ( y ` k ) >. = <. A , ( y ` A ) >. )
77	76	sneqd 4039	. . . . . . . . . . . . . . 15 |- ( k = A -> { <. k , ( y ` k ) >. } = { <. A , ( y ` A ) >. } )
78	77	eqeq2d 2481	. . . . . . . . . . . . . 14 |- ( k = A -> ( y = { <. k , ( y ` k ) >. } <-> y = { <. A , ( y ` A ) >. } ) )
79	74, 78	anbi12d 710	. . . . . . . . . . . . 13 |- ( k = A -> ( ( ( y ` k ) e. X /\ y = { <. k , ( y ` k ) >. } ) <-> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) )
80	9	fsn2 6059	. . . . . . . . . . . . 13 |- ( y : { k } --> X <-> ( ( y ` k ) e. X /\ y = { <. k , ( y ` k ) >. } ) )
81	72, 79, 80	vtoclbg 3172	. . . . . . . . . . . 12 |- ( A e. V -> ( y : { A } --> X <-> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) )
82	71, 81	syl 16	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y : { A } --> X <-> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) )
83	65, 82	mpbid 210	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) )
84	83	simprd 463	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y = { <. A , ( y ` A ) >. } )
85	60	opeq2d 4220	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> <. A , x >. = <. A , ( y ` A ) >. )
86	85	sneqd 4039	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> { <. A , x >. } = { <. A , ( y ` A ) >. } )
87	84, 86	eqtr4d 2511	. . . . . . . 8 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y = { <. A , x >. } )
88	70, 87	jca 532	. . . . . . 7 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( x e. X /\ y = { <. A , x >. } ) )
89	59, 88	impbida 830	. . . . . 6 |- ( ph -> ( ( x e. X /\ y = { <. A , x >. } ) <-> ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) )
90	89	opabbidv 4510	. . . . 5 |- ( ph -> { <. y , x >. | ( x e. X /\ y = { <. A , x >. } ) } = { <. y , x >. | ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) } )
91		df-mpt 4507	. . . . . . 7 |- ( x e. X |-> { <. A , x >. } ) = { <. x , y >. | ( x e. X /\ y = { <. A , x >. } ) }
92	91	cnveqi 5175	. . . . . 6 |- `' ( x e. X |-> { <. A , x >. } ) = `' { <. x , y >. | ( x e. X /\ y = { <. A , x >. } ) }
93		cnvopab 5405	. . . . . 6 |- `' { <. x , y >. | ( x e. X /\ y = { <. A , x >. } ) } = { <. y , x >. | ( x e. X /\ y = { <. A , x >. } ) }
94	92, 93	eqtri 2496	. . . . 5 |- `' ( x e. X |-> { <. A , x >. } ) = { <. y , x >. | ( x e. X /\ y = { <. A , x >. } ) }
95		df-mpt 4507	. . . . 5 |- ( y e. ( X ^m { A } ) |-> ( y ` A ) ) = { <. y , x >. | ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) }
96	90, 94, 95	3eqtr4g 2533	. . . 4 |- ( ph -> `' ( x e. X |-> { <. A , x >. } ) = ( y e. ( X ^m { A } ) |-> ( y ` A ) ) )
97		xpsng 6060	. . . . . . . . . . 11 |- ( ( A e. V /\ J e. (TopOn ` X ) ) -> ( { A } X. { J } ) = { <. A , J >. } )
98	2, 17, 97	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( { A } X. { J } ) = { <. A , J >. } )
99	98	eqcomd 2475	. . . . . . . . 9 |- ( ph -> { <. A , J >. } = ( { A } X. { J } ) )
100	99	fveq2d 5868	. . . . . . . 8 |- ( ph -> ( Xt_ ` { <. A , J >. } ) = ( Xt_ ` ( { A } X. { J } ) ) )
101	16, 100	syl5eq 2520	. . . . . . 7 |- ( ph -> K = ( Xt_ ` ( { A } X. { J } ) ) )
102		eqid 2467	. . . . . . . . 9 |- ( Xt_ ` ( { A } X. { J } ) ) = ( Xt_ ` ( { A } X. { J } ) )
103	102	pttoponconst 19830	. . . . . . . 8 |- ( ( { A } e. _V /\ J e. (TopOn ` X ) ) -> ( Xt_ ` ( { A } X. { J } ) ) e. (TopOn ` ( X ^m { A } ) ) )
104	19, 17, 103	syl2anc 661	. . . . . . 7 |- ( ph -> ( Xt_ ` ( { A } X. { J } ) ) e. (TopOn ` ( X ^m { A } ) ) )
105	101, 104	eqeltrd 2555	. . . . . 6 |- ( ph -> K e. (TopOn ` ( X ^m { A } ) ) )
106		toponuni 19192	. . . . . 6 |- ( K e. (TopOn ` ( X ^m { A } ) ) -> ( X ^m { A } ) = U. K )
107	105, 106	syl 16	. . . . 5 |- ( ph -> ( X ^m { A } ) = U. K )
108	107	mpteq1d 4528	. . . 4 |- ( ph -> ( y e. ( X ^m { A } ) |-> ( y ` A ) ) = ( y e. U. K |-> ( y ` A ) ) )
109	96, 108	eqtrd 2508	. . 3 |- ( ph -> `' ( x e. X |-> { <. A , x >. } ) = ( y e. U. K |-> ( y ` A ) ) )
110		eqid 2467	. . . . . 6 |- U. K = U. K
111	110, 16	ptpjcn 19844	. . . . 5 |- ( ( { A } e. _V /\ { <. A , J >. } : { A } --> Top /\ A e. { A } ) -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn ( { <. A , J >. } ` A ) ) )
112	19, 28, 67, 111	syl3anc 1228	. . . 4 |- ( ph -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn ( { <. A , J >. } ` A ) ) )
113	34	oveq2d 6298	. . . 4 |- ( ph -> ( K Cn ( { <. A , J >. } ` A ) ) = ( K Cn J ) )
114	112, 113	eleqtrd 2557	. . 3 |- ( ph -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn J ) )
115	109, 114	eqeltrd 2555	. 2 |- ( ph -> `' ( x e. X |-> { <. A , x >. } ) e. ( K Cn J ) )
116		ishmeo 19992	. 2 |- ( ( x e. X |-> { <. A , x >. } ) e. ( J Homeo K ) <-> ( ( x e. X |-> { <. A , x >. } ) e. ( J Cn K ) /\ `' ( x e. X |-> { <. A , x >. } ) e. ( K Cn J ) ) )
117	39, 115, 116	sylanbrc 664	1 |- ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Homeo K ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   e. wcel 1767   _Vcvv 3113   C_ wss 3476   {csn 4027   <.cop 4033   U.cuni 4245   {copab 4504   |-> cmpt 4505   X. cxp 4997   `'ccnv 4998   -->wf 5582   -1-1-onto->wf1o 5585   ` cfv 5586  (class class class)co 6282   ^m cmap 7417   Xt_cpt 14687   Topctop 19158  TopOnctopon 19159   Cn ccn 19488   Homeochmeo 19986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-map 7419  df-ixp 7467  df-en 7514  df-dom 7515  df-fin 7517  df-fi 7867  df-topgen 14692  df-pt 14693  df-top 19163  df-bases 19165  df-topon 19166  df-cn 19491  df-cnp 19492  df-hmeo 19988

This theorem is referenced by:  xpstopnlem1  20042  ptcmpfi  20046