Theorem pt1hmeo 17791

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 4880	. . . . 5 |- ( { A } X. { x } ) = ( k e. { A } |-> x )
2		pt1hmeo.a	. . . . . . 7 |- ( ph -> A e. V )
3	2	adantr 452	. . . . . 6 |- ( ( ph /\ x e. X ) -> A e. V )
4		sneq 3785	. . . . . . . . 9 |- ( k = A -> { k } = { A } )
5	4	xpeq1d 4860	. . . . . . . 8 |- ( k = A -> ( { k } X. { x } ) = ( { A } X. { x } ) )
6		opeq1 3944	. . . . . . . . 9 |- ( k = A -> <. k , x >. = <. A , x >. )
7	6	sneqd 3787	. . . . . . . 8 |- ( k = A -> { <. k , x >. } = { <. A , x >. } )
8	5, 7	eqeq12d 2418	. . . . . . 7 |- ( k = A -> ( ( { k } X. { x } ) = { <. k , x >. } <-> ( { A } X. { x } ) = { <. A , x >. } ) )
9		vex 2919	. . . . . . . 8 |- k e. _V
10		vex 2919	. . . . . . . 8 |- x e. _V
11	9, 10	xpsn 5869	. . . . . . 7 |- ( { k } X. { x } ) = { <. k , x >. }
12	8, 11	vtoclg 2971	. . . . . 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 2450	. . . 4 |- ( ( ph /\ x e. X ) -> ( k e. { A } |-> x ) = { <. A , x >. } )
15	14	mpteq2dva 4255	. . 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 4365	. . . . 5 |- { A } e. _V
19	18	a1i 11	. . . 4 |- ( ph -> { A } e. _V )
20		f1osng 5675	. . . . . . 7 |- ( ( A e. V /\ J e. (TopOn ` X ) ) -> { <. A , J >. } : { A } -1-1-onto-> { J } )
21	2, 17, 20	syl2anc 643	. . . . . 6 |- ( ph -> { <. A , J >. } : { A } -1-1-onto-> { J } )
22		f1of 5633	. . . . . 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 16946	. . . . . . 7 |- ( J e. (TopOn ` X ) -> J e. Top )
25	17, 24	syl 16	. . . . . 6 |- ( ph -> J e. Top )
26	25	snssd 3903	. . . . 5 |- ( ph -> { J } C_ Top )
27		fss 5558	. . . . 5 |- ( ( { <. A , J >. } : { A } --> { J } /\ { J } C_ Top ) -> { <. A , J >. } : { A } --> Top )
28	23, 26, 27	syl2anc 643	. . . 4 |- ( ph -> { <. A , J >. } : { A } --> Top )
29	17	cnmptid 17646	. . . . . 6 |- ( ph -> ( x e. X |-> x ) e. ( J Cn J ) )
30	29	adantr 452	. . . . 5 |- ( ( ph /\ k e. { A } ) -> ( x e. X |-> x ) e. ( J Cn J ) )
31		elsni 3798	. . . . . . . 8 |- ( k e. { A } -> k = A )
32	31	fveq2d 5691	. . . . . . 7 |- ( k e. { A } -> ( { <. A , J >. } ` k ) = ( { <. A , J >. } ` A ) )
33		fvsng 5886	. . . . . . . 8 |- ( ( A e. V /\ J e. (TopOn ` X ) ) -> ( { <. A , J >. } ` A ) = J )
34	2, 17, 33	syl2anc 643	. . . . . . 7 |- ( ph -> ( { <. A , J >. } ` A ) = J )
35	32, 34	sylan9eqr 2458	. . . . . 6 |- ( ( ph /\ k e. { A } ) -> ( { <. A , J >. } ` k ) = J )
36	35	oveq2d 6056	. . . . 5 |- ( ( ph /\ k e. { A } ) -> ( J Cn ( { <. A , J >. } ` k ) ) = ( J Cn J ) )
37	30, 36	eleqtrrd 2481	. . . 4 |- ( ( ph /\ k e. { A } ) -> ( x e. X |-> x ) e. ( J Cn ( { <. A , J >. } ` k ) ) )
38	16, 17, 19, 28, 37	ptcn 17612	. . 3 |- ( ph -> ( x e. X |-> ( k e. { A } |-> x ) ) e. ( J Cn K ) )
39	15, 38	eqeltrrd 2479	. 2 |- ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Cn K ) )
40		simprr 734	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y = { <. A , x >. } )
41	14	adantrr 698	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) = { <. A , x >. } )
42	40, 41	eqtr4d 2439	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y = ( k e. { A } |-> x ) )
43		simprl 733	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> x e. X )
44	43	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) /\ k e. { A } ) -> x e. X )
45		eqid 2404	. . . . . . . . . . 11 |- ( k e. { A } |-> x ) = ( k e. { A } |-> x )
46	44, 45	fmptd 5852	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) : { A } --> X )
47		toponmax 16948	. . . . . . . . . . . . 13 |- ( J e. (TopOn ` X ) -> X e. J )
48	17, 47	syl 16	. . . . . . . . . . . 12 |- ( ph -> X e. J )
49	48	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> X e. J )
50		elmapg 6990	. . . . . . . . . . 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 644	. . . . . . . . . 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 224	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) e. ( X ^m { A } ) )
53	42, 52	eqeltrd 2478	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y e. ( X ^m { A } ) )
54	40	fveq1d 5689	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( y ` A ) = ( { <. A , x >. } ` A ) )
55	2	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> A e. V )
56		fvsng 5886	. . . . . . . . . 10 |- ( ( A e. V /\ x e. X ) -> ( { <. A , x >. } ` A ) = x )
57	55, 43, 56	syl2anc 643	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( { <. A , x >. } ` A ) = x )
58	54, 57	eqtr2d 2437	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> x = ( y ` A ) )
59	53, 58	jca 519	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) )
60		simprr 734	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> x = ( y ` A ) )
61		simprl 733	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y e. ( X ^m { A } ) )
62	48	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> X e. J )
63		elmapg 6990	. . . . . . . . . . . 12 |- ( ( X e. J /\ { A } e. _V ) -> ( y e. ( X ^m { A } ) <-> y : { A } --> X ) )
64	62, 18, 63	sylancl 644	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y e. ( X ^m { A } ) <-> y : { A } --> X ) )
65	61, 64	mpbid 202	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y : { A } --> X )
66		snidg 3799	. . . . . . . . . . . 12 |- ( A e. V -> A e. { A } )
67	2, 66	syl 16	. . . . . . . . . . 11 |- ( ph -> A e. { A } )
68	67	adantr 452	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> A e. { A } )
69	65, 68	ffvelrnd 5830	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y ` A ) e. X )
70	60, 69	eqeltrd 2478	. . . . . . . 8 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> x e. X )
71	2	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> A e. V )
72	4	feq2d 5540	. . . . . . . . . . . . 13 |- ( k = A -> ( y : { k } --> X <-> y : { A } --> X ) )
73		fveq2 5687	. . . . . . . . . . . . . . 15 |- ( k = A -> ( y ` k ) = ( y ` A ) )
74	73	eleq1d 2470	. . . . . . . . . . . . . 14 |- ( k = A -> ( ( y ` k ) e. X <-> ( y ` A ) e. X ) )
75		id 20	. . . . . . . . . . . . . . . . 17 |- ( k = A -> k = A )
76	75, 73	opeq12d 3952	. . . . . . . . . . . . . . . 16 |- ( k = A -> <. k , ( y ` k ) >. = <. A , ( y ` A ) >. )
77	76	sneqd 3787	. . . . . . . . . . . . . . 15 |- ( k = A -> { <. k , ( y ` k ) >. } = { <. A , ( y ` A ) >. } )
78	77	eqeq2d 2415	. . . . . . . . . . . . . 14 |- ( k = A -> ( y = { <. k , ( y ` k ) >. } <-> y = { <. A , ( y ` A ) >. } ) )
79	74, 78	anbi12d 692	. . . . . . . . . . . . 13 |- ( k = A -> ( ( ( y ` k ) e. X /\ y = { <. k , ( y ` k ) >. } ) <-> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) )
80	9	fsn2 5867	. . . . . . . . . . . . 13 |- ( y : { k } --> X <-> ( ( y ` k ) e. X /\ y = { <. k , ( y ` k ) >. } ) )
81	72, 79, 80	vtoclbg 2972	. . . . . . . . . . . 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 202	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) )
84	83	simprd 450	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y = { <. A , ( y ` A ) >. } )
85	60	opeq2d 3951	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> <. A , x >. = <. A , ( y ` A ) >. )
86	85	sneqd 3787	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> { <. A , x >. } = { <. A , ( y ` A ) >. } )
87	84, 86	eqtr4d 2439	. . . . . . . 8 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y = { <. A , x >. } )
88	70, 87	jca 519	. . . . . . 7 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( x e. X /\ y = { <. A , x >. } ) )
89	59, 88	impbida 806	. . . . . 6 |- ( ph -> ( ( x e. X /\ y = { <. A , x >. } ) <-> ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) )
90	89	opabbidv 4231	. . . . 5 |- ( ph -> { <. y , x >. | ( x e. X /\ y = { <. A , x >. } ) } = { <. y , x >. | ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) } )
91		df-mpt 4228	. . . . . . 7 |- ( x e. X |-> { <. A , x >. } ) = { <. x , y >. | ( x e. X /\ y = { <. A , x >. } ) }
92	91	cnveqi 5006	. . . . . 6 |- `' ( x e. X |-> { <. A , x >. } ) = `' { <. x , y >. | ( x e. X /\ y = { <. A , x >. } ) }
93		cnvopab 5233	. . . . . 6 |- `' { <. x , y >. | ( x e. X /\ y = { <. A , x >. } ) } = { <. y , x >. | ( x e. X /\ y = { <. A , x >. } ) }
94	92, 93	eqtri 2424	. . . . 5 |- `' ( x e. X |-> { <. A , x >. } ) = { <. y , x >. | ( x e. X /\ y = { <. A , x >. } ) }
95		df-mpt 4228	. . . . 5 |- ( y e. ( X ^m { A } ) |-> ( y ` A ) ) = { <. y , x >. | ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) }
96	90, 94, 95	3eqtr4g 2461	. . . 4 |- ( ph -> `' ( x e. X |-> { <. A , x >. } ) = ( y e. ( X ^m { A } ) |-> ( y ` A ) ) )
97		xpsng 5868	. . . . . . . . . . 11 |- ( ( A e. V /\ J e. (TopOn ` X ) ) -> ( { A } X. { J } ) = { <. A , J >. } )
98	2, 17, 97	syl2anc 643	. . . . . . . . . 10 |- ( ph -> ( { A } X. { J } ) = { <. A , J >. } )
99	98	eqcomd 2409	. . . . . . . . 9 |- ( ph -> { <. A , J >. } = ( { A } X. { J } ) )
100	99	fveq2d 5691	. . . . . . . 8 |- ( ph -> ( Xt_ ` { <. A , J >. } ) = ( Xt_ ` ( { A } X. { J } ) ) )
101	16, 100	syl5eq 2448	. . . . . . 7 |- ( ph -> K = ( Xt_ ` ( { A } X. { J } ) ) )
102		eqid 2404	. . . . . . . . 9 |- ( Xt_ ` ( { A } X. { J } ) ) = ( Xt_ ` ( { A } X. { J } ) )
103	102	pttoponconst 17582	. . . . . . . 8 |- ( ( { A } e. _V /\ J e. (TopOn ` X ) ) -> ( Xt_ ` ( { A } X. { J } ) ) e. (TopOn ` ( X ^m { A } ) ) )
104	19, 17, 103	syl2anc 643	. . . . . . 7 |- ( ph -> ( Xt_ ` ( { A } X. { J } ) ) e. (TopOn ` ( X ^m { A } ) ) )
105	101, 104	eqeltrd 2478	. . . . . 6 |- ( ph -> K e. (TopOn ` ( X ^m { A } ) ) )
106		toponuni 16947	. . . . . 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 4250	. . . 4 |- ( ph -> ( y e. ( X ^m { A } ) |-> ( y ` A ) ) = ( y e. U. K |-> ( y ` A ) ) )
109	96, 108	eqtrd 2436	. . 3 |- ( ph -> `' ( x e. X |-> { <. A , x >. } ) = ( y e. U. K |-> ( y ` A ) ) )
110		eqid 2404	. . . . . 6 |- U. K = U. K
111	110, 16	ptpjcn 17596	. . . . 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 1184	. . . 4 |- ( ph -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn ( { <. A , J >. } ` A ) ) )
113	34	oveq2d 6056	. . . 4 |- ( ph -> ( K Cn ( { <. A , J >. } ` A ) ) = ( K Cn J ) )
114	112, 113	eleqtrd 2480	. . 3 |- ( ph -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn J ) )
115	109, 114	eqeltrd 2478	. 2 |- ( ph -> `' ( x e. X |-> { <. A , x >. } ) e. ( K Cn J ) )
116		ishmeo 17744	. 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 646	1 |- ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Homeo K ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   _Vcvv 2916   C_ wss 3280   {csn 3774   <.cop 3777   U.cuni 3975   {copab 4225   e. cmpt 4226   X. cxp 4835   `'ccnv 4836   -->wf 5409   -1-1-onto->wf1o 5412   ` cfv 5413  (class class class)co 6040   ^m cmap 6977   Xt_cpt 13621   Topctop 16913  TopOnctopon 16914   Cn ccn 17242   Homeo chmeo 17738

This theorem is referenced by:  xpstopnlem1  17794  ptcmpfi  17798

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-recs 6592  df-rdg 6627  df-1o 6683  df-oadd 6687  df-er 6864  df-map 6979  df-ixp 7023  df-en 7069  df-dom 7070  df-fin 7072  df-fi 7374  df-topgen 13622  df-pt 13623  df-top 16918  df-bases 16920  df-topon 16921  df-cn 17245  df-cnp 17246  df-hmeo 17740