fmptsng

Description: Express a singleton function in maps-to notation. Version of fmptsn allowing the value B to depend on the variable x . (Contributed by AV, 27-Feb-2019)

		Ref	Expression
	Hypothesis	fmptsng.1	$⊢ x = A \to B = C$
	Assertion	fmptsng	$⊢ (A \in V \land C \in W) \to \{⟨A, C⟩\} = (x \in \{A\} ⟼ B)$

Proof

Step	Hyp	Ref	Expression
1		fmptsng.1	$⊢ x = A \to B = C$
2		velsn	$⊢ x \in \{A\} \leftrightarrow x = A$
3	2	bicomi	$⊢ x = A \leftrightarrow x \in \{A\}$
4	3	anbi1i	$⊢ (x = A \land y = B) \leftrightarrow (x \in \{A\} \land y = B)$
5	4	opabbii	$⊢ \{⟨x, y⟩ \| (x = A \land y = B)\} = \{⟨x, y⟩ \| (x \in \{A\} \land y = B)\}$
6		velsn	$⊢ p \in \{⟨A, C⟩\} \leftrightarrow p = ⟨A, C⟩$
7		eqidd	$⊢ (A \in V \land C \in W) \to A = A$
8		eqidd	$⊢ (A \in V \land C \in W) \to C = C$
9		eqeq1	$⊢ x = A \to (x = A \leftrightarrow A = A)$
10	9	adantr	$⊢ (x = A \land y = C) \to (x = A \leftrightarrow A = A)$
11		eqeq1	$⊢ y = C \to (y = B \leftrightarrow C = B)$
12	1	eqeq2d	$⊢ x = A \to (C = B \leftrightarrow C = C)$
13	11 12	sylan9bbr	$⊢ (x = A \land y = C) \to (y = B \leftrightarrow C = C)$
14	10 13	anbi12d	$⊢ (x = A \land y = C) \to ((x = A \land y = B) \leftrightarrow (A = A \land C = C))$
15	14	opelopabga	$⊢ (A \in V \land C \in W) \to (⟨A, C⟩ \in \{⟨x, y⟩ \| (x = A \land y = B)\} \leftrightarrow (A = A \land C = C))$
16	7 8 15	mpbir2and	$⊢ (A \in V \land C \in W) \to ⟨A, C⟩ \in \{⟨x, y⟩ \| (x = A \land y = B)\}$
17		eleq1	$⊢ p = ⟨A, C⟩ \to (p \in \{⟨x, y⟩ \| (x = A \land y = B)\} \leftrightarrow ⟨A, C⟩ \in \{⟨x, y⟩ \| (x = A \land y = B)\})$
18	16 17	syl5ibrcom	$⊢ (A \in V \land C \in W) \to (p = ⟨A, C⟩ \to p \in \{⟨x, y⟩ \| (x = A \land y = B)\})$
19	6 18	syl5bi	$⊢ (A \in V \land C \in W) \to (p \in \{⟨A, C⟩\} \to p \in \{⟨x, y⟩ \| (x = A \land y = B)\})$
20		elopab	$⊢ p \in \{⟨x, y⟩ \| (x = A \land y = B)\} \leftrightarrow \exists x \exists y (p = ⟨x, y⟩ \land (x = A \land y = B))$
21		opeq12	$⊢ (x = A \land y = B) \to ⟨x, y⟩ = ⟨A, B⟩$
22	21	eqeq2d	$⊢ (x = A \land y = B) \to (p = ⟨x, y⟩ \leftrightarrow p = ⟨A, B⟩)$
23	1	adantr	$⊢ (x = A \land y = B) \to B = C$
24	23	opeq2d	$⊢ (x = A \land y = B) \to ⟨A, B⟩ = ⟨A, C⟩$
25		opex	$⊢ ⟨A, C⟩ \in V$
26	25	snid	$⊢ ⟨A, C⟩ \in \{⟨A, C⟩\}$
27	24 26	eqeltrdi	$⊢ (x = A \land y = B) \to ⟨A, B⟩ \in \{⟨A, C⟩\}$
28		eleq1	$⊢ p = ⟨A, B⟩ \to (p \in \{⟨A, C⟩\} \leftrightarrow ⟨A, B⟩ \in \{⟨A, C⟩\})$
29	27 28	syl5ibrcom	$⊢ (x = A \land y = B) \to (p = ⟨A, B⟩ \to p \in \{⟨A, C⟩\})$
30	22 29	sylbid	$⊢ (x = A \land y = B) \to (p = ⟨x, y⟩ \to p \in \{⟨A, C⟩\})$
31	30	impcom	$⊢ (p = ⟨x, y⟩ \land (x = A \land y = B)) \to p \in \{⟨A, C⟩\}$
32	31	exlimivv	$⊢ \exists x \exists y (p = ⟨x, y⟩ \land (x = A \land y = B)) \to p \in \{⟨A, C⟩\}$
33	32	a1i	$⊢ (A \in V \land C \in W) \to (\exists x \exists y (p = ⟨x, y⟩ \land (x = A \land y = B)) \to p \in \{⟨A, C⟩\})$
34	20 33	syl5bi	$⊢ (A \in V \land C \in W) \to (p \in \{⟨x, y⟩ \| (x = A \land y = B)\} \to p \in \{⟨A, C⟩\})$
35	19 34	impbid	$⊢ (A \in V \land C \in W) \to (p \in \{⟨A, C⟩\} \leftrightarrow p \in \{⟨x, y⟩ \| (x = A \land y = B)\})$
36	35	eqrdv	$⊢ (A \in V \land C \in W) \to \{⟨A, C⟩\} = \{⟨x, y⟩ \| (x = A \land y = B)\}$
37		df-mpt	$⊢ (x \in \{A\} ⟼ B) = \{⟨x, y⟩ \| (x \in \{A\} \land y = B)\}$
38	37	a1i	$⊢ (A \in V \land C \in W) \to (x \in \{A\} ⟼ B) = \{⟨x, y⟩ \| (x \in \{A\} \land y = B)\}$
39	5 36 38	3eqtr4a	$⊢ (A \in V \land C \in W) \to \{⟨A, C⟩\} = (x \in \{A\} ⟼ B)$

Metamath Proof Explorer

Theorem fmptsng

Proof