Metamath Proof Explorer

Theorem pt1hmeo

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)

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

Proof

Step Hyp Ref Expression
1 pt1hmeo.j 
 |-  K = ( Xt_ ` { <. A , J >. } )
2 pt1hmeo.a 
 |-  ( ph -> A e. V )
3 pt1hmeo.r 
 |-  ( ph -> J e. ( TopOn ` X ) )
4 fconstmpt 
 |-  ( { A } X. { x } ) = ( k e. { A } |-> x )
5 2 adantr 
 |-  ( ( ph /\ x e. X ) -> A e. V )
6 sneq 
 |-  ( k = A -> { k } = { A } )
7 6 xpeq1d 
 |-  ( k = A -> ( { k } X. { x } ) = ( { A } X. { x } ) )
8 opeq1 
 |-  ( k = A -> <. k , x >. = <. A , x >. )
9 8 sneqd 
 |-  ( k = A -> { <. k , x >. } = { <. A , x >. } )
10 7 9 eqeq12d 
 |-  ( k = A -> ( ( { k } X. { x } ) = { <. k , x >. } <-> ( { A } X. { x } ) = { <. A , x >. } ) )
11 vex 
 |-  k e. _V
12 vex 
 |-  x e. _V
13 11 12 xpsn 
 |-  ( { k } X. { x } ) = { <. k , x >. }
14 10 13 vtoclg 
 |-  ( A e. V -> ( { A } X. { x } ) = { <. A , x >. } )
15 5 14 syl 
 |-  ( ( ph /\ x e. X ) -> ( { A } X. { x } ) = { <. A , x >. } )
16 4 15 eqtr3id 
 |-  ( ( ph /\ x e. X ) -> ( k e. { A } |-> x ) = { <. A , x >. } )
17 16 mpteq2dva 
 |-  ( ph -> ( x e. X |-> ( k e. { A } |-> x ) ) = ( x e. X |-> { <. A , x >. } ) )
18 snex 
 |-  { A } e. _V
19 18 a1i 
 |-  ( ph -> { A } e. _V )
20 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
21 3 20 syl 
 |-  ( ph -> J e. Top )
22 2 21 fsnd 
 |-  ( ph -> { <. A , J >. } : { A } --> Top )
23 3 cnmptid 
 |-  ( ph -> ( x e. X |-> x ) e. ( J Cn J ) )
24 23 adantr 
 |-  ( ( ph /\ k e. { A } ) -> ( x e. X |-> x ) e. ( J Cn J ) )
25 elsni 
 |-  ( k e. { A } -> k = A )
26 25 fveq2d 
 |-  ( k e. { A } -> ( { <. A , J >. } ` k ) = ( { <. A , J >. } ` A ) )
27 fvsng 
 |-  ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( { <. A , J >. } ` A ) = J )
28 2 3 27 syl2anc 
 |-  ( ph -> ( { <. A , J >. } ` A ) = J )
29 26 28 sylan9eqr 
 |-  ( ( ph /\ k e. { A } ) -> ( { <. A , J >. } ` k ) = J )
30 29 oveq2d 
 |-  ( ( ph /\ k e. { A } ) -> ( J Cn ( { <. A , J >. } ` k ) ) = ( J Cn J ) )
31 24 30 eleqtrrd 
 |-  ( ( ph /\ k e. { A } ) -> ( x e. X |-> x ) e. ( J Cn ( { <. A , J >. } ` k ) ) )
32 1 3 19 22 31 ptcn 
 |-  ( ph -> ( x e. X |-> ( k e. { A } |-> x ) ) e. ( J Cn K ) )
33 17 32 eqeltrrd 
 |-  ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Cn K ) )
34 simprr 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y = { <. A , x >. } )
35 16 adantrr 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) = { <. A , x >. } )
36 34 35 eqtr4d 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y = ( k e. { A } |-> x ) )
37 simprl 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> x e. X )
38 37 adantr 
 |-  ( ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) /\ k e. { A } ) -> x e. X )
39 38 fmpttd 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) : { A } --> X )
40 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
41 3 40 syl 
 |-  ( ph -> X e. J )
42 41 adantr 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> X e. J )
43 elmapg 
 |-  ( ( X e. J /\ { A } e. _V ) -> ( ( k e. { A } |-> x ) e. ( X ^m { A } ) <-> ( k e. { A } |-> x ) : { A } --> X ) )
44 42 18 43 sylancl 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( ( k e. { A } |-> x ) e. ( X ^m { A } ) <-> ( k e. { A } |-> x ) : { A } --> X ) )
45 39 44 mpbird 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( k e. { A } |-> x ) e. ( X ^m { A } ) )
46 36 45 eqeltrd 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> y e. ( X ^m { A } ) )
47 34 fveq1d 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( y ` A ) = ( { <. A , x >. } ` A ) )
48 2 adantr 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> A e. V )
49 fvsng 
 |-  ( ( A e. V /\ x e. X ) -> ( { <. A , x >. } ` A ) = x )
50 48 37 49 syl2anc 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( { <. A , x >. } ` A ) = x )
51 47 50 eqtr2d 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> x = ( y ` A ) )
52 46 51 jca 
 |-  ( ( ph /\ ( x e. X /\ y = { <. A , x >. } ) ) -> ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) )
53 simprr 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> x = ( y ` A ) )
54 simprl 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y e. ( X ^m { A } ) )
55 41 adantr 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> X e. J )
56 elmapg 
 |-  ( ( X e. J /\ { A } e. _V ) -> ( y e. ( X ^m { A } ) <-> y : { A } --> X ) )
57 55 18 56 sylancl 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y e. ( X ^m { A } ) <-> y : { A } --> X ) )
58 54 57 mpbid 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y : { A } --> X )
59 snidg 
 |-  ( A e. V -> A e. { A } )
60 2 59 syl 
 |-  ( ph -> A e. { A } )
61 60 adantr 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> A e. { A } )
62 58 61 ffvelrnd 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y ` A ) e. X )
63 53 62 eqeltrd 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> x e. X )
64 2 adantr 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> A e. V )
65 fsn2g 
 |-  ( A e. V -> ( y : { A } --> X <-> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) )
66 64 65 syl 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( y : { A } --> X <-> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) ) )
67 58 66 mpbid 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( ( y ` A ) e. X /\ y = { <. A , ( y ` A ) >. } ) )
68 67 simprd 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y = { <. A , ( y ` A ) >. } )
69 53 opeq2d 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> <. A , x >. = <. A , ( y ` A ) >. )
70 69 sneqd 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> { <. A , x >. } = { <. A , ( y ` A ) >. } )
71 68 70 eqtr4d 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> y = { <. A , x >. } )
72 63 71 jca 
 |-  ( ( ph /\ ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) -> ( x e. X /\ y = { <. A , x >. } ) )
73 52 72 impbida 
 |-  ( ph -> ( ( x e. X /\ y = { <. A , x >. } ) <-> ( y e. ( X ^m { A } ) /\ x = ( y ` A ) ) ) )
74 73 mptcnv 
 |-  ( ph -> `' ( x e. X |-> { <. A , x >. } ) = ( y e. ( X ^m { A } ) |-> ( y ` A ) ) )
75 xpsng 
 |-  ( ( A e. V /\ J e. ( TopOn ` X ) ) -> ( { A } X. { J } ) = { <. A , J >. } )
76 2 3 75 syl2anc 
 |-  ( ph -> ( { A } X. { J } ) = { <. A , J >. } )
77 76 eqcomd 
 |-  ( ph -> { <. A , J >. } = ( { A } X. { J } ) )
78 77 fveq2d 
 |-  ( ph -> ( Xt_ ` { <. A , J >. } ) = ( Xt_ ` ( { A } X. { J } ) ) )
79 1 78 syl5eq 
 |-  ( ph -> K = ( Xt_ ` ( { A } X. { J } ) ) )
80 eqid 
 |-  ( Xt_ ` ( { A } X. { J } ) ) = ( Xt_ ` ( { A } X. { J } ) )
81 80 pttoponconst 
 |-  ( ( { A } e. _V /\ J e. ( TopOn ` X ) ) -> ( Xt_ ` ( { A } X. { J } ) ) e. ( TopOn ` ( X ^m { A } ) ) )
82 19 3 81 syl2anc 
 |-  ( ph -> ( Xt_ ` ( { A } X. { J } ) ) e. ( TopOn ` ( X ^m { A } ) ) )
83 79 82 eqeltrd 
 |-  ( ph -> K e. ( TopOn ` ( X ^m { A } ) ) )
84 toponuni 
 |-  ( K e. ( TopOn ` ( X ^m { A } ) ) -> ( X ^m { A } ) = U. K )
85 83 84 syl 
 |-  ( ph -> ( X ^m { A } ) = U. K )
86 85 mpteq1d 
 |-  ( ph -> ( y e. ( X ^m { A } ) |-> ( y ` A ) ) = ( y e. U. K |-> ( y ` A ) ) )
87 74 86 eqtrd 
 |-  ( ph -> `' ( x e. X |-> { <. A , x >. } ) = ( y e. U. K |-> ( y ` A ) ) )
88 eqid 
 |-  U. K = U. K
89 88 1 ptpjcn 
 |-  ( ( { A } e. _V /\ { <. A , J >. } : { A } --> Top /\ A e. { A } ) -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn ( { <. A , J >. } ` A ) ) )
90 18 22 60 89 mp3an2i 
 |-  ( ph -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn ( { <. A , J >. } ` A ) ) )
91 28 oveq2d 
 |-  ( ph -> ( K Cn ( { <. A , J >. } ` A ) ) = ( K Cn J ) )
92 90 91 eleqtrd 
 |-  ( ph -> ( y e. U. K |-> ( y ` A ) ) e. ( K Cn J ) )
93 87 92 eqeltrd 
 |-  ( ph -> `' ( x e. X |-> { <. A , x >. } ) e. ( K Cn J ) )
94 ishmeo 
 |-  ( ( 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 ) ) )
95 33 93 94 sylanbrc 
 |-  ( ph -> ( x e. X |-> { <. A , x >. } ) e. ( J Homeo K ) )