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 = \prod_{𝑡} (\{⟨A, J⟩\})$
	pt1hmeo.a	$⊢ φ \to A \in V$
	pt1hmeo.r	$⊢ φ \to J \in TopOn (X)$
Assertion	pt1hmeo	$⊢ φ \to (x \in X ⟼ \{⟨A, x⟩\}) \in (J Homeo K)$

Proof

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

Metamath Proof Explorer

Theorem pt1hmeo

Proof