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	syl5eqr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑘 ∈ { 𝐴 } ↦ 𝑥 ) = { ⟨ 𝐴 , 𝑥 ⟩ } )
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 𝐾 ) )