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 ) )