Theorem pt1hmeo 21609

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

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 5163	. . . . 5 |- ( { A } X. { x } ) = ( k e. { A } |-> x )
2		pt1hmeo.a	. . . . . . 7 |- ( ph -> A e. V )
3	2	adantr 481	. . . . . 6 |- ( ( ph /\ x e. X ) -> A e. V )
4		sneq 4187	. . . . . . . . 9 |- ( k = A -> { k } = { A } )
5	4	xpeq1d 5138	. . . . . . . 8 |- ( k = A -> ( { k } X. { x } ) = ( { A } X. { x } ) )
6		opeq1 4402	. . . . . . . . 9 |- ( k = A -> <. k , x >. = <. A , x >. )
7	6	sneqd 4189	. . . . . . . 8 |- ( k = A -> { <. k , x >. } = { <. A , x >. } )
8	5, 7	eqeq12d 2637	. . . . . . 7 |- ( k = A -> ( ( { k } X. { x } ) = { <. k , x >. } <-> ( { A } X. { x } ) = { <. A , x >. } ) )
9		vex 3203	. . . . . . . 8 |- k e. _V
10		vex 3203	. . . . . . . 8 |- x e. _V
11	9, 10	xpsn 6407	. . . . . . 7 |- ( { k } X. { x } ) = { <. k , x >. }
12	8, 11	vtoclg 3266	. . . . . 6 |- ( A e. V -> ( { A } X. { x } ) = { <. A , x >. } )
13	3, 12	syl 17	. . . . 5 |- ( ( ph /\ x e. X ) -> ( { A } X. { x } ) = { <. A , x >. } )
14	1, 13	syl5eqr 2670	. . . 4 |- ( ( ph /\ x e. X ) -> ( k e. { A } |-> x ) = { <. A , x >. } )
15	14	mpteq2dva 4744	. . 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 4908	. . . . 5 |- { A } e. _V
19	18	a1i 11	. . . 4 |- ( ph -> { A } e. _V )
20		topontop 20718	. . . . . 6 |- ( J e. (TopOn ` X ) -> J e. Top )
21	17, 20	syl 17	. . . . 5 |- ( ph -> J e. Top )
22	2, 21	fsnd 6179	. . . 4 |- ( ph -> { <. A , J >. } : { A } --> Top )
23	17	cnmptid 21464	. . . . . 6 |- ( ph -> ( x e. X |-> x ) e. ( J Cn J ) )
24	23	adantr 481	. . . . 5 |- ( ( ph /\ k e. { A } ) -> ( x e. X |-> x ) e. ( J Cn J ) )
25		elsni 4194	. . . . . . . 8 |- ( k e. { A } -> k = A )
26	25	fveq2d 6195	. . . . . . 7 |- ( k e. { A } -> ( { <. A , J >. } ` k ) = ( { <. A , J >. } ` A ) )
27		fvsng 6447	. . . . . . . 8 |- ( ( A e. V /\ J e. (TopOn ` X ) ) -> ( { <. A , J >. } ` A ) = J )
28	2, 17, 27	syl2anc 693	. . . . . . 7 |- ( ph -> ( { <. A , J >. } ` A ) = J )
29	26, 28	sylan9eqr 2678	. . . . . 6 |- ( ( ph /\ k e. { A } ) -> ( { <. A , J >. } ` k ) = J )
30	29	oveq2d 6666	. . . . 5 |- ( ( ph /\ k e. { A } ) -> ( J Cn ( { <. A , J >. } ` k ) ) = ( J Cn J ) )
31	24, 30	eleqtrrd 2704	. . . 4 |- ( ( ph /\ k e. { A } ) -> ( x e. X |-> x ) e. ( J Cn ( { <. A , J >. } ` k ) ) )
32	16, 17, 19, 22, 31	ptcn 21430	. . 3 |- ( ph -> ( x e. X |-> ( k e. { A } |-> x ) ) e. ( J Cn K ) )
33	15, 32	eqeltrrd 2702	. 2 |- ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Cn K ) )
34		simprr 796	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y = { <. A , x >. } )
35	14	adantrr 753	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) = { <. A , x >. } )
36	34, 35	eqtr4d 2659	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y = ( k e. { A } |-> x ) )
37		simprl 794	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> x e. X )
38	37	adantr 481	. . . . . . . . . 10 |- ( ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) /\ k e. { A } ) -> x e. X )
39		eqid 2622	. . . . . . . . . 10 |- ( k e. { A } |-> x ) = ( k e. { A } |-> x )
40	38, 39	fmptd 6385	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) : { A } --> X )
41		toponmax 20730	. . . . . . . . . . . 12 |- ( J e. (TopOn ` X ) -> X e. J )
42	17, 41	syl 17	. . . . . . . . . . 11 |- ( ph -> X e. J )
43	42	adantr 481	. . . . . . . . . 10 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> X e. J )
44		elmapg 7870	. . . . . . . . . 10 |- ( ( X e. J /\ { A } e. _V ) -> ( ( k e. { A } |-> x ) e. ( X ^m { A } ) <-> ( k e. { A } |-> x ) : { A } --> X ) )
45	43, 18, 44	sylancl 694	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( ( k e. { A } |-> x ) e. ( X ^m { A } ) <-> ( k e. { A } |-> x ) : { A } --> X ) )
46	40, 45	mpbird 247	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) e. ( X ^m { A } ) )
47	36, 46	eqeltrd 2701	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y e. ( X ^m { A } ) )
48	34	fveq1d 6193	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( y ` A ) = ( { <. A , x >. } ` A ) )
49	2	adantr 481	. . . . . . . . 9 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> A e. V )
50		fvsng 6447	. . . . . . . . 9 |- ( ( A e. V /\ x e. X ) -> ( { <. A , x >. } ` A ) = x )
51	49, 37, 50	syl2anc 693	. . . . . . . 8 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( { <. A , x >. } ` A ) = x )
52	48, 51	eqtr2d 2657	. . . . . . 7 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> x = ( y ` A ) )
53	47, 52	jca 554	. . . . . 6 |- ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) )
54		simprr 796	. . . . . . . 8 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> x = ( y ` A ) )
55		simprl 794	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y e. ( X ^m { A } ) )
56	42	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> X e. J )
57		elmapg 7870	. . . . . . . . . . 11 |- ( ( X e. J /\ { A } e. _V ) -> ( y e. ( X ^m { A } ) <-> y : { A } --> X ) )
58	56, 18, 57	sylancl 694	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y e. ( X ^m { A } ) <-> y : { A } --> X ) )
59	55, 58	mpbid 222	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y : { A } --> X )
60		snidg 4206	. . . . . . . . . . 11 |- ( A e. V -> A e. { A } )
61	2, 60	syl 17	. . . . . . . . . 10 |- ( ph -> A e. { A } )
62	61	adantr 481	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> A e. { A } )
63	59, 62	ffvelrnd 6360	. . . . . . . 8 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y ` A ) e. X )
64	54, 63	eqeltrd 2701	. . . . . . 7 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> x e. X )
65	2	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> A e. V )
66		fsn2g 6405	. . . . . . . . . . 11 |- ( A e. V -> ( y : { A } --> X <-> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) )
67	65, 66	syl 17	. . . . . . . . . 10 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y : { A } --> X <-> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) )
68	59, 67	mpbid 222	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) )
69	68	simprd 479	. . . . . . . 8 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y = { <. A , ( y ` A ) >. } )
70	54	opeq2d 4409	. . . . . . . . 9 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> <. A , x >. = <. A , ( y ` A ) >. )
71	70	sneqd 4189	. . . . . . . 8 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> { <. A , x >. } = { <. A , ( y ` A ) >. } )
72	69, 71	eqtr4d 2659	. . . . . . 7 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y = { <. A , x >. } )
73	64, 72	jca 554	. . . . . 6 |- ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( x e. X /\ y = { <. A , x >. } ) )
74	53, 73	impbida 877	. . . . 5 |- ( ph -> ( ( x e. X /\ y = { <. A , x >. } ) <-> ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) )
75	74	mptcnv 5534	. . . 4 |- ( ph -> `' ( x e. X |-> { <. A , x >. } ) = ( y e. ( X ^m { A } ) |-> ( y ` A ) ) )
76		xpsng 6406	. . . . . . . . . . 11 |- ( ( A e. V /\ J e. (TopOn ` X ) ) -> ( { A } X. { J } ) = { <. A , J >. } )
77	2, 17, 76	syl2anc 693	. . . . . . . . . 10 |- ( ph -> ( { A } X. { J } ) = { <. A , J >. } )
78	77	eqcomd 2628	. . . . . . . . 9 |- ( ph -> { <. A , J >. } = ( { A } X. { J } ) )
79	78	fveq2d 6195	. . . . . . . 8 |- ( ph -> ( Xt_ ` { <. A , J >. } ) = ( Xt_ ` ( { A } X. { J } ) ) )
80	16, 79	syl5eq 2668	. . . . . . 7 |- ( ph -> K = ( Xt_ ` ( { A } X. { J } ) ) )
81		eqid 2622	. . . . . . . . 9 |- ( Xt_ ` ( { A } X. { J } ) ) = ( Xt_ ` ( { A } X. { J } ) )
82	81	pttoponconst 21400	. . . . . . . 8 |- ( ( { A } e. _V /\ J e. (TopOn ` X ) ) -> ( Xt_ ` ( { A } X. { J } ) ) e. (TopOn ` ( X ^m { A } ) ) )
83	19, 17, 82	syl2anc 693	. . . . . . 7 |- ( ph -> ( Xt_ ` ( { A } X. { J } ) ) e. (TopOn ` ( X ^m { A } ) ) )
84	80, 83	eqeltrd 2701	. . . . . 6 |- ( ph -> K e. (TopOn ` ( X ^m { A } ) ) )
85		toponuni 20719	. . . . . 6 |- ( K e. (TopOn ` ( X ^m { A } ) ) -> ( X ^m { A } ) = U. K )
86	84, 85	syl 17	. . . . 5 |- ( ph -> ( X ^m { A } ) = U. K )
87	86	mpteq1d 4738	. . . 4 |- ( ph -> ( y e. ( X ^m { A } ) |-> ( y ` A ) ) = ( y e. U. K |-> ( y ` A ) ) )
88	75, 87	eqtrd 2656	. . 3 |- ( ph -> `' ( x e. X |-> { <. A , x >. } ) = ( y e. U. K |-> ( y ` A ) ) )
89		eqid 2622	. . . . . 6 |- U. K = U. K
90	89, 16	ptpjcn 21414	. . . . 5 |- ( ( { A } e. _V /\ { <. A , J >. } : { A } --> Top /\ A e. { A } ) -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn ( { <. A , J >. } ` A ) ) )
91	18, 22, 61, 90	mp3an2i 1429	. . . 4 |- ( ph -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn ( { <. A , J >. } ` A ) ) )
92	28	oveq2d 6666	. . . 4 |- ( ph -> ( K Cn ( { <. A , J >. } ` A ) ) = ( K Cn J ) )
93	91, 92	eleqtrd 2703	. . 3 |- ( ph -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn J ) )
94	88, 93	eqeltrd 2701	. 2 |- ( ph -> `' ( x e. X |-> { <. A , x >. } ) e. ( K Cn J ) )
95		ishmeo 21562	. 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 ) ) )
96	33, 94, 95	sylanbrc 698	1 |- ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Homeo K ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   _Vcvv 3200   {csn 4177   <.cop 4183   U.cuni 4436   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   -->wf 5884   ` cfv 5888  (class class class)co 6650   ^m cmap 7857   Xt_cpt 16099   Topctop 20698  TopOnctopon 20715   Cn ccn 21028   Homeochmeo 21556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-ixp 7909  df-en 7956  df-dom 7957  df-fin 7959  df-fi 8317  df-topgen 16104  df-pt 16105  df-top 20699  df-topon 20716  df-bases 20750  df-cn 21031  df-cnp 21032  df-hmeo 21558

This theorem is referenced by:  xpstopnlem1  21612  ptcmpfi  21616