mapsnend

Description: Set exponentiation to a singleton exponent is equinumerous to its base. Exercise 4.43 of Mendelson p. 255. (Contributed by NM, 17-Dec-2003) (Revised by Mario Carneiro, 15-Nov-2014) (Revised by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	mapsnend.a	$⊢ φ \to A \in V$
	mapsnend.b	$⊢ φ \to B \in W$
Assertion	mapsnend	$⊢ φ \to (A^{\{B\}}) \approx A$

Proof

Step	Hyp	Ref	Expression
1		mapsnend.a	$⊢ φ \to A \in V$
2		mapsnend.b	$⊢ φ \to B \in W$
3		ovexd	$⊢ φ \to A^{\{B\}} \in V$
4		fvexd	$⊢ z \in (A^{\{B\}}) \to z (B) \in V$
5	4	a1i	$⊢ φ \to (z \in (A^{\{B\}}) \to z (B) \in V)$
6		snex	$⊢ \{⟨B, w⟩\} \in V$
7	6	2a1i	$⊢ φ \to (w \in A \to \{⟨B, w⟩\} \in V)$
8	1 2	mapsnd	$⊢ φ \to A^{\{B\}} = \{z \| \exists y \in A z = \{⟨B, y⟩\}\}$
9	8	eqabrd	$⊢ φ \to (z \in (A^{\{B\}}) \leftrightarrow \exists y \in A z = \{⟨B, y⟩\})$
10	9	anbi1d	$⊢ φ \to ((z \in (A^{\{B\}}) \land w = z (B)) \leftrightarrow (\exists y \in A z = \{⟨B, y⟩\} \land w = z (B)))$
11		r19.41v	$⊢ \exists y \in A (z = \{⟨B, y⟩\} \land w = z (B)) \leftrightarrow (\exists y \in A z = \{⟨B, y⟩\} \land w = z (B))$
12	11	bicomi	$⊢ (\exists y \in A z = \{⟨B, y⟩\} \land w = z (B)) \leftrightarrow \exists y \in A (z = \{⟨B, y⟩\} \land w = z (B))$
13	12	a1i	$⊢ φ \to ((\exists y \in A z = \{⟨B, y⟩\} \land w = z (B)) \leftrightarrow \exists y \in A (z = \{⟨B, y⟩\} \land w = z (B)))$
14		df-rex	$⊢ \exists y \in A (z = \{⟨B, y⟩\} \land w = z (B)) \leftrightarrow \exists y (y \in A \land (z = \{⟨B, y⟩\} \land w = z (B)))$
15	14	a1i	$⊢ φ \to (\exists y \in A (z = \{⟨B, y⟩\} \land w = z (B)) \leftrightarrow \exists y (y \in A \land (z = \{⟨B, y⟩\} \land w = z (B))))$
16	10 13 15	3bitrd	$⊢ φ \to ((z \in (A^{\{B\}}) \land w = z (B)) \leftrightarrow \exists y (y \in A \land (z = \{⟨B, y⟩\} \land w = z (B))))$
17		fveq1	$⊢ z = \{⟨B, y⟩\} \to z (B) = \{⟨B, y⟩\} (B)$
18		vex	$⊢ y \in V$
19		fvsng	$⊢ (B \in W \land y \in V) \to \{⟨B, y⟩\} (B) = y$
20	2 18 19	sylancl	$⊢ φ \to \{⟨B, y⟩\} (B) = y$
21	17 20	sylan9eqr	$⊢ (φ \land z = \{⟨B, y⟩\}) \to z (B) = y$
22	21	eqeq2d	$⊢ (φ \land z = \{⟨B, y⟩\}) \to (w = z (B) \leftrightarrow w = y)$
23		equcom	$⊢ w = y \leftrightarrow y = w$
24	22 23	bitrdi	$⊢ (φ \land z = \{⟨B, y⟩\}) \to (w = z (B) \leftrightarrow y = w)$
25	24	pm5.32da	$⊢ φ \to ((z = \{⟨B, y⟩\} \land w = z (B)) \leftrightarrow (z = \{⟨B, y⟩\} \land y = w))$
26	25	anbi2d	$⊢ φ \to ((y \in A \land (z = \{⟨B, y⟩\} \land w = z (B))) \leftrightarrow (y \in A \land (z = \{⟨B, y⟩\} \land y = w)))$
27		anass	$⊢ ((y \in A \land z = \{⟨B, y⟩\}) \land y = w) \leftrightarrow (y \in A \land (z = \{⟨B, y⟩\} \land y = w))$
28	27	a1i	$⊢ φ \to (((y \in A \land z = \{⟨B, y⟩\}) \land y = w) \leftrightarrow (y \in A \land (z = \{⟨B, y⟩\} \land y = w)))$
29		ancom	$⊢ ((y \in A \land z = \{⟨B, y⟩\}) \land y = w) \leftrightarrow (y = w \land (y \in A \land z = \{⟨B, y⟩\}))$
30	29	a1i	$⊢ φ \to (((y \in A \land z = \{⟨B, y⟩\}) \land y = w) \leftrightarrow (y = w \land (y \in A \land z = \{⟨B, y⟩\})))$
31	26 28 30	3bitr2d	$⊢ φ \to ((y \in A \land (z = \{⟨B, y⟩\} \land w = z (B))) \leftrightarrow (y = w \land (y \in A \land z = \{⟨B, y⟩\})))$
32	31	exbidv	$⊢ φ \to (\exists y (y \in A \land (z = \{⟨B, y⟩\} \land w = z (B))) \leftrightarrow \exists y (y = w \land (y \in A \land z = \{⟨B, y⟩\})))$
33		eleq1w	$⊢ y = w \to (y \in A \leftrightarrow w \in A)$
34		opeq2	$⊢ y = w \to ⟨B, y⟩ = ⟨B, w⟩$
35	34	sneqd	$⊢ y = w \to \{⟨B, y⟩\} = \{⟨B, w⟩\}$
36	35	eqeq2d	$⊢ y = w \to (z = \{⟨B, y⟩\} \leftrightarrow z = \{⟨B, w⟩\})$
37	33 36	anbi12d	$⊢ y = w \to ((y \in A \land z = \{⟨B, y⟩\}) \leftrightarrow (w \in A \land z = \{⟨B, w⟩\}))$
38	37	equsexvw	$⊢ \exists y (y = w \land (y \in A \land z = \{⟨B, y⟩\})) \leftrightarrow (w \in A \land z = \{⟨B, w⟩\})$
39	38	a1i	$⊢ φ \to (\exists y (y = w \land (y \in A \land z = \{⟨B, y⟩\})) \leftrightarrow (w \in A \land z = \{⟨B, w⟩\}))$
40	16 32 39	3bitrd	$⊢ φ \to ((z \in (A^{\{B\}}) \land w = z (B)) \leftrightarrow (w \in A \land z = \{⟨B, w⟩\}))$
41	3 1 5 7 40	en2d	$⊢ φ \to (A^{\{B\}}) \approx A$

Metamath Proof Explorer

Theorem mapsnend

Proof