mapsnd

Description: The value of set exponentiation with a singleton exponent. Theorem 98 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Revised by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	mapsnd.1	$⊢ φ \to A \in V$
	mapsnd.2	$⊢ φ \to B \in W$
Assertion	mapsnd	$⊢ φ \to A^{\{B\}} = \{f \| \exists y \in A f = \{⟨B, y⟩\}\}$

Proof

Step	Hyp	Ref	Expression
1		mapsnd.1	$⊢ φ \to A \in V$
2		mapsnd.2	$⊢ φ \to B \in W$
3		snex	$⊢ \{B\} \in V$
4	3	a1i	$⊢ φ \to \{B\} \in V$
5	1 4	elmapd	$⊢ φ \to (f \in (A^{\{B\}}) \leftrightarrow f : \{B\} ⟶ A)$
6		ffn	$⊢ f : \{B\} ⟶ A \to f Fn \{B\}$
7		snidg	$⊢ B \in W \to B \in \{B\}$
8	2 7	syl	$⊢ φ \to B \in \{B\}$
9		fneu	$⊢ (f Fn \{B\} \land B \in \{B\}) \to \exists! y B f y$
10	6 8 9	syl2anr	$⊢ (φ \land f : \{B\} ⟶ A) \to \exists! y B f y$
11		euabsn	$⊢ \exists! y B f y \leftrightarrow \exists y \{y \| B f y\} = \{y\}$
12		frel	$⊢ f : \{B\} ⟶ A \to Rel f$
13		relimasn	$⊢ Rel f \to f [\{B\}] = \{y \| B f y\}$
14	12 13	syl	$⊢ f : \{B\} ⟶ A \to f [\{B\}] = \{y \| B f y\}$
15		fdm	$⊢ f : \{B\} ⟶ A \to dom f = \{B\}$
16	15	imaeq2d	$⊢ f : \{B\} ⟶ A \to f [dom f] = f [\{B\}]$
17		imadmrn	$⊢ f [dom f] = ran f$
18	16 17	eqtr3di	$⊢ f : \{B\} ⟶ A \to f [\{B\}] = ran f$
19	14 18	eqtr3d	$⊢ f : \{B\} ⟶ A \to \{y \| B f y\} = ran f$
20	19	eqeq1d	$⊢ f : \{B\} ⟶ A \to (\{y \| B f y\} = \{y\} \leftrightarrow ran f = \{y\})$
21	20	exbidv	$⊢ f : \{B\} ⟶ A \to (\exists y \{y \| B f y\} = \{y\} \leftrightarrow \exists y ran f = \{y\})$
22	11 21	bitrid	$⊢ f : \{B\} ⟶ A \to (\exists! y B f y \leftrightarrow \exists y ran f = \{y\})$
23	22	adantl	$⊢ (φ \land f : \{B\} ⟶ A) \to (\exists! y B f y \leftrightarrow \exists y ran f = \{y\})$
24	10 23	mpbid	$⊢ (φ \land f : \{B\} ⟶ A) \to \exists y ran f = \{y\}$
25		frn	$⊢ f : \{B\} ⟶ A \to ran f \subseteq A$
26	25	sseld	$⊢ f : \{B\} ⟶ A \to (y \in ran f \to y \in A)$
27		vsnid	$⊢ y \in \{y\}$
28		eleq2	$⊢ ran f = \{y\} \to (y \in ran f \leftrightarrow y \in \{y\})$
29	27 28	mpbiri	$⊢ ran f = \{y\} \to y \in ran f$
30	26 29	impel	$⊢ (f : \{B\} ⟶ A \land ran f = \{y\}) \to y \in A$
31	30	adantll	$⊢ ((φ \land f : \{B\} ⟶ A) \land ran f = \{y\}) \to y \in A$
32		ffrn	$⊢ f : \{B\} ⟶ A \to f : \{B\} ⟶ ran f$
33		feq3	$⊢ ran f = \{y\} \to (f : \{B\} ⟶ ran f \leftrightarrow f : \{B\} ⟶ \{y\})$
34	32 33	syl5ibcom	$⊢ f : \{B\} ⟶ A \to (ran f = \{y\} \to f : \{B\} ⟶ \{y\})$
35	34	imp	$⊢ (f : \{B\} ⟶ A \land ran f = \{y\}) \to f : \{B\} ⟶ \{y\}$
36	35	adantll	$⊢ ((φ \land f : \{B\} ⟶ A) \land ran f = \{y\}) \to f : \{B\} ⟶ \{y\}$
37	2	ad2antrr	$⊢ ((φ \land f : \{B\} ⟶ A) \land ran f = \{y\}) \to B \in W$
38		vex	$⊢ y \in V$
39		fsng	$⊢ (B \in W \land y \in V) \to (f : \{B\} ⟶ \{y\} \leftrightarrow f = \{⟨B, y⟩\})$
40	37 38 39	sylancl	$⊢ ((φ \land f : \{B\} ⟶ A) \land ran f = \{y\}) \to (f : \{B\} ⟶ \{y\} \leftrightarrow f = \{⟨B, y⟩\})$
41	36 40	mpbid	$⊢ ((φ \land f : \{B\} ⟶ A) \land ran f = \{y\}) \to f = \{⟨B, y⟩\}$
42	31 41	jca	$⊢ ((φ \land f : \{B\} ⟶ A) \land ran f = \{y\}) \to (y \in A \land f = \{⟨B, y⟩\})$
43	42	ex	$⊢ (φ \land f : \{B\} ⟶ A) \to (ran f = \{y\} \to (y \in A \land f = \{⟨B, y⟩\}))$
44	43	eximdv	$⊢ (φ \land f : \{B\} ⟶ A) \to (\exists y ran f = \{y\} \to \exists y (y \in A \land f = \{⟨B, y⟩\}))$
45	24 44	mpd	$⊢ (φ \land f : \{B\} ⟶ A) \to \exists y (y \in A \land f = \{⟨B, y⟩\})$
46		df-rex	$⊢ \exists y \in A f = \{⟨B, y⟩\} \leftrightarrow \exists y (y \in A \land f = \{⟨B, y⟩\})$
47	45 46	sylibr	$⊢ (φ \land f : \{B\} ⟶ A) \to \exists y \in A f = \{⟨B, y⟩\}$
48	47	ex	$⊢ φ \to (f : \{B\} ⟶ A \to \exists y \in A f = \{⟨B, y⟩\})$
49		f1osng	$⊢ (B \in W \land y \in V) \to \{⟨B, y⟩\} : \{B\} \underset{1-1 onto}{⟶} \{y\}$
50	2 38 49	sylancl	$⊢ φ \to \{⟨B, y⟩\} : \{B\} \underset{1-1 onto}{⟶} \{y\}$
51	50	adantr	$⊢ (φ \land f = \{⟨B, y⟩\}) \to \{⟨B, y⟩\} : \{B\} \underset{1-1 onto}{⟶} \{y\}$
52		f1oeq1	$⊢ f = \{⟨B, y⟩\} \to (f : \{B\} \underset{1-1 onto}{⟶} \{y\} \leftrightarrow \{⟨B, y⟩\} : \{B\} \underset{1-1 onto}{⟶} \{y\})$
53	52	bicomd	$⊢ f = \{⟨B, y⟩\} \to (\{⟨B, y⟩\} : \{B\} \underset{1-1 onto}{⟶} \{y\} \leftrightarrow f : \{B\} \underset{1-1 onto}{⟶} \{y\})$
54	53	adantl	$⊢ (φ \land f = \{⟨B, y⟩\}) \to (\{⟨B, y⟩\} : \{B\} \underset{1-1 onto}{⟶} \{y\} \leftrightarrow f : \{B\} \underset{1-1 onto}{⟶} \{y\})$
55	51 54	mpbid	$⊢ (φ \land f = \{⟨B, y⟩\}) \to f : \{B\} \underset{1-1 onto}{⟶} \{y\}$
56		f1of	$⊢ f : \{B\} \underset{1-1 onto}{⟶} \{y\} \to f : \{B\} ⟶ \{y\}$
57	55 56	syl	$⊢ (φ \land f = \{⟨B, y⟩\}) \to f : \{B\} ⟶ \{y\}$
58	57	3adant2	$⊢ (φ \land y \in A \land f = \{⟨B, y⟩\}) \to f : \{B\} ⟶ \{y\}$
59		snssi	$⊢ y \in A \to \{y\} \subseteq A$
60	59	3ad2ant2	$⊢ (φ \land y \in A \land f = \{⟨B, y⟩\}) \to \{y\} \subseteq A$
61	58 60	fssd	$⊢ (φ \land y \in A \land f = \{⟨B, y⟩\}) \to f : \{B\} ⟶ A$
62	61	rexlimdv3a	$⊢ φ \to (\exists y \in A f = \{⟨B, y⟩\} \to f : \{B\} ⟶ A)$
63	48 62	impbid	$⊢ φ \to (f : \{B\} ⟶ A \leftrightarrow \exists y \in A f = \{⟨B, y⟩\})$
64	5 63	bitrd	$⊢ φ \to (f \in (A^{\{B\}}) \leftrightarrow \exists y \in A f = \{⟨B, y⟩\})$
65	64	eqabdv	$⊢ φ \to A^{\{B\}} = \{f \| \exists y \in A f = \{⟨B, y⟩\}\}$

Metamath Proof Explorer

Theorem mapsnd

Proof