This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝑋 ↑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 eqtrid ⊢ ( 𝜑 → 𝐾 = ( ∏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 𝐾 ) )