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 𝐾 = ( ∏t ‘ { ⟨ 𝐴 , 𝐽 ⟩ } )
pt1hmeo.a ( 𝜑𝐴𝑉 )
pt1hmeo.r ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
Assertion pt1hmeo ( 𝜑 → ( 𝑥𝑋 ↦ { ⟨ 𝐴 , 𝑥 ⟩ } ) ∈ ( 𝐽 Homeo 𝐾 ) )

Proof

Step Hyp Ref Expression
1 pt1hmeo.j 𝐾 = ( ∏t ‘ { ⟨ 𝐴 , 𝐽 ⟩ } )
2 pt1hmeo.a ( 𝜑𝐴𝑉 )
3 pt1hmeo.r ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 fconstmpt ( { 𝐴 } × { 𝑥 } ) = ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 )
5 2 adantr ( ( 𝜑𝑥𝑋 ) → 𝐴𝑉 )
6 sneq ( 𝑘 = 𝐴 → { 𝑘 } = { 𝐴 } )
7 6 xpeq1d ( 𝑘 = 𝐴 → ( { 𝑘 } × { 𝑥 } ) = ( { 𝐴 } × { 𝑥 } ) )
8 opeq1 ( 𝑘 = 𝐴 → ⟨ 𝑘 , 𝑥 ⟩ = ⟨ 𝐴 , 𝑥 ⟩ )
9 8 sneqd ( 𝑘 = 𝐴 → { ⟨ 𝑘 , 𝑥 ⟩ } = { ⟨ 𝐴 , 𝑥 ⟩ } )
10 7 9 eqeq12d ( 𝑘 = 𝐴 → ( ( { 𝑘 } × { 𝑥 } ) = { ⟨ 𝑘 , 𝑥 ⟩ } ↔ ( { 𝐴 } × { 𝑥 } ) = { ⟨ 𝐴 , 𝑥 ⟩ } ) )
11 vex 𝑘 ∈ V
12 vex 𝑥 ∈ V
13 11 12 xpsn ( { 𝑘 } × { 𝑥 } ) = { ⟨ 𝑘 , 𝑥 ⟩ }
14 10 13 vtoclg ( 𝐴𝑉 → ( { 𝐴 } × { 𝑥 } ) = { ⟨ 𝐴 , 𝑥 ⟩ } )
15 5 14 syl ( ( 𝜑𝑥𝑋 ) → ( { 𝐴 } × { 𝑥 } ) = { ⟨ 𝐴 , 𝑥 ⟩ } )
16 4 15 eqtr3id ( ( 𝜑𝑥𝑋 ) → ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) = { ⟨ 𝐴 , 𝑥 ⟩ } )
17 16 mpteq2dva ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) ) = ( 𝑥𝑋 ↦ { ⟨ 𝐴 , 𝑥 ⟩ } ) )
18 snex { 𝐴 } ∈ V
19 18 a1i ( 𝜑 → { 𝐴 } ∈ V )
20 topontop ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
21 3 20 syl ( 𝜑𝐽 ∈ Top )
22 2 21 fsnd ( 𝜑 → { ⟨ 𝐴 , 𝐽 ⟩ } : { 𝐴 } ⟶ Top )
23 3 cnmptid ( 𝜑 → ( 𝑥𝑋𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
24 23 adantr ( ( 𝜑𝑘 ∈ { 𝐴 } ) → ( 𝑥𝑋𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
25 elsni ( 𝑘 ∈ { 𝐴 } → 𝑘 = 𝐴 )
26 25 fveq2d ( 𝑘 ∈ { 𝐴 } → ( { ⟨ 𝐴 , 𝐽 ⟩ } ‘ 𝑘 ) = ( { ⟨ 𝐴 , 𝐽 ⟩ } ‘ 𝐴 ) )
27 fvsng ( ( 𝐴𝑉𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( { ⟨ 𝐴 , 𝐽 ⟩ } ‘ 𝐴 ) = 𝐽 )
28 2 3 27 syl2anc ( 𝜑 → ( { ⟨ 𝐴 , 𝐽 ⟩ } ‘ 𝐴 ) = 𝐽 )
29 26 28 sylan9eqr ( ( 𝜑𝑘 ∈ { 𝐴 } ) → ( { ⟨ 𝐴 , 𝐽 ⟩ } ‘ 𝑘 ) = 𝐽 )
30 29 oveq2d ( ( 𝜑𝑘 ∈ { 𝐴 } ) → ( 𝐽 Cn ( { ⟨ 𝐴 , 𝐽 ⟩ } ‘ 𝑘 ) ) = ( 𝐽 Cn 𝐽 ) )
31 24 30 eleqtrrd ( ( 𝜑𝑘 ∈ { 𝐴 } ) → ( 𝑥𝑋𝑥 ) ∈ ( 𝐽 Cn ( { ⟨ 𝐴 , 𝐽 ⟩ } ‘ 𝑘 ) ) )
32 1 3 19 22 31 ptcn ( 𝜑 → ( 𝑥𝑋 ↦ ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) ) ∈ ( 𝐽 Cn 𝐾 ) )
33 17 32 eqeltrrd ( 𝜑 → ( 𝑥𝑋 ↦ { ⟨ 𝐴 , 𝑥 ⟩ } ) ∈ ( 𝐽 Cn 𝐾 ) )
34 simprr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → 𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } )
35 16 adantrr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) = { ⟨ 𝐴 , 𝑥 ⟩ } )
36 34 35 eqtr4d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → 𝑦 = ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) )
37 simprl ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → 𝑥𝑋 )
38 37 adantr ( ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) ∧ 𝑘 ∈ { 𝐴 } ) → 𝑥𝑋 )
39 38 fmpttd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) : { 𝐴 } ⟶ 𝑋 )
40 toponmax ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋𝐽 )
41 3 40 syl ( 𝜑𝑋𝐽 )
42 41 adantr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → 𝑋𝐽 )
43 elmapg ( ( 𝑋𝐽 ∧ { 𝐴 } ∈ V ) → ( ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) ∈ ( 𝑋m { 𝐴 } ) ↔ ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) : { 𝐴 } ⟶ 𝑋 ) )
44 42 18 43 sylancl ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → ( ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) ∈ ( 𝑋m { 𝐴 } ) ↔ ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) : { 𝐴 } ⟶ 𝑋 ) )
45 39 44 mpbird ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) ∈ ( 𝑋m { 𝐴 } ) )
46 36 45 eqeltrd ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → 𝑦 ∈ ( 𝑋m { 𝐴 } ) )
47 34 fveq1d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → ( 𝑦𝐴 ) = ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) )
48 2 adantr ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → 𝐴𝑉 )
49 fvsng ( ( 𝐴𝑉𝑥𝑋 ) → ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) = 𝑥 )
50 48 37 49 syl2anc ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → ( { ⟨ 𝐴 , 𝑥 ⟩ } ‘ 𝐴 ) = 𝑥 )
51 47 50 eqtr2d ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → 𝑥 = ( 𝑦𝐴 ) )
52 46 51 jca ( ( 𝜑 ∧ ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ) → ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) )
53 simprr ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → 𝑥 = ( 𝑦𝐴 ) )
54 simprl ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → 𝑦 ∈ ( 𝑋m { 𝐴 } ) )
55 41 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → 𝑋𝐽 )
56 elmapg ( ( 𝑋𝐽 ∧ { 𝐴 } ∈ V ) → ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ↔ 𝑦 : { 𝐴 } ⟶ 𝑋 ) )
57 55 18 56 sylancl ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ↔ 𝑦 : { 𝐴 } ⟶ 𝑋 ) )
58 54 57 mpbid ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → 𝑦 : { 𝐴 } ⟶ 𝑋 )
59 snidg ( 𝐴𝑉𝐴 ∈ { 𝐴 } )
60 2 59 syl ( 𝜑𝐴 ∈ { 𝐴 } )
61 60 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → 𝐴 ∈ { 𝐴 } )
62 58 61 ffvelrnd ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → ( 𝑦𝐴 ) ∈ 𝑋 )
63 53 62 eqeltrd ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → 𝑥𝑋 )
64 2 adantr ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → 𝐴𝑉 )
65 fsn2g ( 𝐴𝑉 → ( 𝑦 : { 𝐴 } ⟶ 𝑋 ↔ ( ( 𝑦𝐴 ) ∈ 𝑋𝑦 = { ⟨ 𝐴 , ( 𝑦𝐴 ) ⟩ } ) ) )
66 64 65 syl ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → ( 𝑦 : { 𝐴 } ⟶ 𝑋 ↔ ( ( 𝑦𝐴 ) ∈ 𝑋𝑦 = { ⟨ 𝐴 , ( 𝑦𝐴 ) ⟩ } ) ) )
67 58 66 mpbid ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → ( ( 𝑦𝐴 ) ∈ 𝑋𝑦 = { ⟨ 𝐴 , ( 𝑦𝐴 ) ⟩ } ) )
68 67 simprd ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → 𝑦 = { ⟨ 𝐴 , ( 𝑦𝐴 ) ⟩ } )
69 53 opeq2d ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → ⟨ 𝐴 , 𝑥 ⟩ = ⟨ 𝐴 , ( 𝑦𝐴 ) ⟩ )
70 69 sneqd ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → { ⟨ 𝐴 , 𝑥 ⟩ } = { ⟨ 𝐴 , ( 𝑦𝐴 ) ⟩ } )
71 68 70 eqtr4d ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → 𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } )
72 63 71 jca ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) → ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) )
73 52 72 impbida ( 𝜑 → ( ( 𝑥𝑋𝑦 = { ⟨ 𝐴 , 𝑥 ⟩ } ) ↔ ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ∧ 𝑥 = ( 𝑦𝐴 ) ) ) )
74 73 mptcnv ( 𝜑 ( 𝑥𝑋 ↦ { ⟨ 𝐴 , 𝑥 ⟩ } ) = ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ↦ ( 𝑦𝐴 ) ) )
75 xpsng ( ( 𝐴𝑉𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( { 𝐴 } × { 𝐽 } ) = { ⟨ 𝐴 , 𝐽 ⟩ } )
76 2 3 75 syl2anc ( 𝜑 → ( { 𝐴 } × { 𝐽 } ) = { ⟨ 𝐴 , 𝐽 ⟩ } )
77 76 eqcomd ( 𝜑 → { ⟨ 𝐴 , 𝐽 ⟩ } = ( { 𝐴 } × { 𝐽 } ) )
78 77 fveq2d ( 𝜑 → ( ∏t ‘ { ⟨ 𝐴 , 𝐽 ⟩ } ) = ( ∏t ‘ ( { 𝐴 } × { 𝐽 } ) ) )
79 1 78 syl5eq ( 𝜑𝐾 = ( ∏t ‘ ( { 𝐴 } × { 𝐽 } ) ) )
80 eqid ( ∏t ‘ ( { 𝐴 } × { 𝐽 } ) ) = ( ∏t ‘ ( { 𝐴 } × { 𝐽 } ) )
81 80 pttoponconst ( ( { 𝐴 } ∈ V ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( ∏t ‘ ( { 𝐴 } × { 𝐽 } ) ) ∈ ( TopOn ‘ ( 𝑋m { 𝐴 } ) ) )
82 19 3 81 syl2anc ( 𝜑 → ( ∏t ‘ ( { 𝐴 } × { 𝐽 } ) ) ∈ ( TopOn ‘ ( 𝑋m { 𝐴 } ) ) )
83 79 82 eqeltrd ( 𝜑𝐾 ∈ ( TopOn ‘ ( 𝑋m { 𝐴 } ) ) )
84 toponuni ( 𝐾 ∈ ( TopOn ‘ ( 𝑋m { 𝐴 } ) ) → ( 𝑋m { 𝐴 } ) = 𝐾 )
85 83 84 syl ( 𝜑 → ( 𝑋m { 𝐴 } ) = 𝐾 )
86 85 mpteq1d ( 𝜑 → ( 𝑦 ∈ ( 𝑋m { 𝐴 } ) ↦ ( 𝑦𝐴 ) ) = ( 𝑦 𝐾 ↦ ( 𝑦𝐴 ) ) )
87 74 86 eqtrd ( 𝜑 ( 𝑥𝑋 ↦ { ⟨ 𝐴 , 𝑥 ⟩ } ) = ( 𝑦 𝐾 ↦ ( 𝑦𝐴 ) ) )
88 eqid 𝐾 = 𝐾
89 88 1 ptpjcn ( ( { 𝐴 } ∈ V ∧ { ⟨ 𝐴 , 𝐽 ⟩ } : { 𝐴 } ⟶ Top ∧ 𝐴 ∈ { 𝐴 } ) → ( 𝑦 𝐾 ↦ ( 𝑦𝐴 ) ) ∈ ( 𝐾 Cn ( { ⟨ 𝐴 , 𝐽 ⟩ } ‘ 𝐴 ) ) )
90 18 22 60 89 mp3an2i ( 𝜑 → ( 𝑦 𝐾 ↦ ( 𝑦𝐴 ) ) ∈ ( 𝐾 Cn ( { ⟨ 𝐴 , 𝐽 ⟩ } ‘ 𝐴 ) ) )
91 28 oveq2d ( 𝜑 → ( 𝐾 Cn ( { ⟨ 𝐴 , 𝐽 ⟩ } ‘ 𝐴 ) ) = ( 𝐾 Cn 𝐽 ) )
92 90 91 eleqtrd ( 𝜑 → ( 𝑦 𝐾 ↦ ( 𝑦𝐴 ) ) ∈ ( 𝐾 Cn 𝐽 ) )
93 87 92 eqeltrd ( 𝜑 ( 𝑥𝑋 ↦ { ⟨ 𝐴 , 𝑥 ⟩ } ) ∈ ( 𝐾 Cn 𝐽 ) )
94 ishmeo ( ( 𝑥𝑋 ↦ { ⟨ 𝐴 , 𝑥 ⟩ } ) ∈ ( 𝐽 Homeo 𝐾 ) ↔ ( ( 𝑥𝑋 ↦ { ⟨ 𝐴 , 𝑥 ⟩ } ) ∈ ( 𝐽 Cn 𝐾 ) ∧ ( 𝑥𝑋 ↦ { ⟨ 𝐴 , 𝑥 ⟩ } ) ∈ ( 𝐾 Cn 𝐽 ) ) )
95 33 93 94 sylanbrc ( 𝜑 → ( 𝑥𝑋 ↦ { ⟨ 𝐴 , 𝑥 ⟩ } ) ∈ ( 𝐽 Homeo 𝐾 ) )