mapsncnv

Description: Expression for the inverse of the canonical map between a set and its set of singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	mapsncnv.s	$⊢ S = \{X\}$
	mapsncnv.b	$⊢ B \in V$
	mapsncnv.x	$⊢ X \in V$
	mapsncnv.f	$⊢ F = (x \in (B^{S}) ⟼ x (X))$
Assertion	mapsncnv	$⊢ F^{-1} = (y \in B ⟼ S \times \{y\})$

Proof

Step	Hyp	Ref	Expression
1		mapsncnv.s	$⊢ S = \{X\}$
2		mapsncnv.b	$⊢ B \in V$
3		mapsncnv.x	$⊢ X \in V$
4		mapsncnv.f	$⊢ F = (x \in (B^{S}) ⟼ x (X))$
5		elmapi	$⊢ x \in (B^{\{X\}}) \to x : \{X\} ⟶ B$
6	3	snid	$⊢ X \in \{X\}$
7		ffvelcdm	$⊢ (x : \{X\} ⟶ B \land X \in \{X\}) \to x (X) \in B$
8	5 6 7	sylancl	$⊢ x \in (B^{\{X\}}) \to x (X) \in B$
9		eqid	$⊢ \{X\} = \{X\}$
10	9 2 3	mapsnconst	$⊢ x \in (B^{\{X\}}) \to x = \{X\} \times \{x (X)\}$
11	8 10	jca	$⊢ x \in (B^{\{X\}}) \to (x (X) \in B \land x = \{X\} \times \{x (X)\})$
12		eleq1	$⊢ y = x (X) \to (y \in B \leftrightarrow x (X) \in B)$
13		sneq	$⊢ y = x (X) \to \{y\} = \{x (X)\}$
14	13	xpeq2d	$⊢ y = x (X) \to \{X\} \times \{y\} = \{X\} \times \{x (X)\}$
15	14	eqeq2d	$⊢ y = x (X) \to (x = \{X\} \times \{y\} \leftrightarrow x = \{X\} \times \{x (X)\})$
16	12 15	anbi12d	$⊢ y = x (X) \to ((y \in B \land x = \{X\} \times \{y\}) \leftrightarrow (x (X) \in B \land x = \{X\} \times \{x (X)\}))$
17	11 16	syl5ibrcom	$⊢ x \in (B^{\{X\}}) \to (y = x (X) \to (y \in B \land x = \{X\} \times \{y\}))$
18	17	imp	$⊢ (x \in (B^{\{X\}}) \land y = x (X)) \to (y \in B \land x = \{X\} \times \{y\})$
19		fconst6g	$⊢ y \in B \to (\{X\} \times \{y\}) : \{X\} ⟶ B$
20		snex	$⊢ \{X\} \in V$
21	2 20	elmap	$⊢ \{X\} \times \{y\} \in (B^{\{X\}}) \leftrightarrow (\{X\} \times \{y\}) : \{X\} ⟶ B$
22	19 21	sylibr	$⊢ y \in B \to \{X\} \times \{y\} \in (B^{\{X\}})$
23		vex	$⊢ y \in V$
24	23	fvconst2	$⊢ X \in \{X\} \to (\{X\} \times \{y\}) (X) = y$
25	6 24	mp1i	$⊢ y \in B \to (\{X\} \times \{y\}) (X) = y$
26	25	eqcomd	$⊢ y \in B \to y = (\{X\} \times \{y\}) (X)$
27	22 26	jca	$⊢ y \in B \to (\{X\} \times \{y\} \in (B^{\{X\}}) \land y = (\{X\} \times \{y\}) (X))$
28		eleq1	$⊢ x = \{X\} \times \{y\} \to (x \in (B^{\{X\}}) \leftrightarrow \{X\} \times \{y\} \in (B^{\{X\}}))$
29		fveq1	$⊢ x = \{X\} \times \{y\} \to x (X) = (\{X\} \times \{y\}) (X)$
30	29	eqeq2d	$⊢ x = \{X\} \times \{y\} \to (y = x (X) \leftrightarrow y = (\{X\} \times \{y\}) (X))$
31	28 30	anbi12d	$⊢ x = \{X\} \times \{y\} \to ((x \in (B^{\{X\}}) \land y = x (X)) \leftrightarrow (\{X\} \times \{y\} \in (B^{\{X\}}) \land y = (\{X\} \times \{y\}) (X)))$
32	27 31	syl5ibrcom	$⊢ y \in B \to (x = \{X\} \times \{y\} \to (x \in (B^{\{X\}}) \land y = x (X)))$
33	32	imp	$⊢ (y \in B \land x = \{X\} \times \{y\}) \to (x \in (B^{\{X\}}) \land y = x (X))$
34	18 33	impbii	$⊢ (x \in (B^{\{X\}}) \land y = x (X)) \leftrightarrow (y \in B \land x = \{X\} \times \{y\})$
35	1	oveq2i	$⊢ B^{S} = B^{\{X\}}$
36	35	eleq2i	$⊢ x \in (B^{S}) \leftrightarrow x \in (B^{\{X\}})$
37	36	anbi1i	$⊢ (x \in (B^{S}) \land y = x (X)) \leftrightarrow (x \in (B^{\{X\}}) \land y = x (X))$
38	1	xpeq1i	$⊢ S \times \{y\} = \{X\} \times \{y\}$
39	38	eqeq2i	$⊢ x = S \times \{y\} \leftrightarrow x = \{X\} \times \{y\}$
40	39	anbi2i	$⊢ (y \in B \land x = S \times \{y\}) \leftrightarrow (y \in B \land x = \{X\} \times \{y\})$
41	34 37 40	3bitr4i	$⊢ (x \in (B^{S}) \land y = x (X)) \leftrightarrow (y \in B \land x = S \times \{y\})$
42	41	opabbii	$⊢ \{⟨y, x⟩ \| (x \in (B^{S}) \land y = x (X))\} = \{⟨y, x⟩ \| (y \in B \land x = S \times \{y\})\}$
43		df-mpt	$⊢ (x \in (B^{S}) ⟼ x (X)) = \{⟨x, y⟩ \| (x \in (B^{S}) \land y = x (X))\}$
44	4 43	eqtri	$⊢ F = \{⟨x, y⟩ \| (x \in (B^{S}) \land y = x (X))\}$
45	44	cnveqi	$⊢ F^{-1} = {\{⟨x, y⟩ \| (x \in (B^{S}) \land y = x (X))\}}^{-1}$
46		cnvopab	$⊢ {\{⟨x, y⟩ \| (x \in (B^{S}) \land y = x (X))\}}^{-1} = \{⟨y, x⟩ \| (x \in (B^{S}) \land y = x (X))\}$
47	45 46	eqtri	$⊢ F^{-1} = \{⟨y, x⟩ \| (x \in (B^{S}) \land y = x (X))\}$
48		df-mpt	$⊢ (y \in B ⟼ S \times \{y\}) = \{⟨y, x⟩ \| (y \in B \land x = S \times \{y\})\}$
49	42 47 48	3eqtr4i	$⊢ F^{-1} = (y \in B ⟼ S \times \{y\})$

Metamath Proof Explorer

Theorem mapsncnv

Proof