# 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 )`
` |-  ( ( 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 syl5eqr
` |-  ( ( 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 ) )`
` |-  ( ( 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 >. } )`
` |-  ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 } ) )`
` |-  ( ( 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 } )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) )`