mposn

Description: An operation (in maps-to notation) on two singletons. (Contributed by AV, 4-Aug-2019)

	Ref	Expression
Hypotheses	mposn.f	$⊢ F = (x \in \{A\}, y \in \{B\} ⟼ C)$
	mposn.a	$⊢ x = A \to C = D$
	mposn.b	$⊢ y = B \to D = E$
Assertion	mposn	$⊢ (A \in V \land B \in W \land E \in U) \to F = \{⟨⟨A, B⟩, E⟩\}$

Proof

Step	Hyp	Ref	Expression
1		mposn.f	$⊢ F = (x \in \{A\}, y \in \{B\} ⟼ C)$
2		mposn.a	$⊢ x = A \to C = D$
3		mposn.b	$⊢ y = B \to D = E$
4		xpsng	$⊢ (A \in V \land B \in W) \to \{A\} \times \{B\} = \{⟨A, B⟩\}$
5	4	3adant3	$⊢ (A \in V \land B \in W \land E \in U) \to \{A\} \times \{B\} = \{⟨A, B⟩\}$
6	5	mpteq1d	$⊢ (A \in V \land B \in W \land E \in U) \to (p \in (\{A\} \times \{B\}) ⟼ ⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C) = (p \in \{⟨A, B⟩\} ⟼ ⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C)$
7		mpompts	$⊢ (x \in \{A\}, y \in \{B\} ⟼ C) = (p \in (\{A\} \times \{B\}) ⟼ ⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C)$
8	1 7	eqtri	$⊢ F = (p \in (\{A\} \times \{B\}) ⟼ ⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C)$
9	8	a1i	$⊢ (A \in V \land B \in W \land E \in U) \to F = (p \in (\{A\} \times \{B\}) ⟼ ⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C)$
10		op2ndg	$⊢ (A \in V \land B \in W) \to 2^{nd} (⟨A, B⟩) = B$
11		fveq2	$⊢ p = ⟨A, B⟩ \to 2^{nd} (p) = 2^{nd} (⟨A, B⟩)$
12	11	eqcomd	$⊢ p = ⟨A, B⟩ \to 2^{nd} (⟨A, B⟩) = 2^{nd} (p)$
13	12	eqeq1d	$⊢ p = ⟨A, B⟩ \to (2^{nd} (⟨A, B⟩) = B \leftrightarrow 2^{nd} (p) = B)$
14	10 13	syl5ibcom	$⊢ (A \in V \land B \in W) \to (p = ⟨A, B⟩ \to 2^{nd} (p) = B)$
15	14	3adant3	$⊢ (A \in V \land B \in W \land E \in U) \to (p = ⟨A, B⟩ \to 2^{nd} (p) = B)$
16	15	imp	$⊢ ((A \in V \land B \in W \land E \in U) \land p = ⟨A, B⟩) \to 2^{nd} (p) = B$
17		op1stg	$⊢ (A \in V \land B \in W) \to 1^{st} (⟨A, B⟩) = A$
18		fveq2	$⊢ p = ⟨A, B⟩ \to 1^{st} (p) = 1^{st} (⟨A, B⟩)$
19	18	eqcomd	$⊢ p = ⟨A, B⟩ \to 1^{st} (⟨A, B⟩) = 1^{st} (p)$
20	19	eqeq1d	$⊢ p = ⟨A, B⟩ \to (1^{st} (⟨A, B⟩) = A \leftrightarrow 1^{st} (p) = A)$
21	17 20	syl5ibcom	$⊢ (A \in V \land B \in W) \to (p = ⟨A, B⟩ \to 1^{st} (p) = A)$
22	21	3adant3	$⊢ (A \in V \land B \in W \land E \in U) \to (p = ⟨A, B⟩ \to 1^{st} (p) = A)$
23	22	imp	$⊢ ((A \in V \land B \in W \land E \in U) \land p = ⟨A, B⟩) \to 1^{st} (p) = A$
24		simp1	$⊢ (A \in V \land B \in W \land E \in U) \to A \in V$
25		simpl2	$⊢ ((A \in V \land B \in W \land E \in U) \land x = A) \to B \in W$
26	2	adantl	$⊢ ((A \in V \land B \in W \land E \in U) \land x = A) \to C = D$
27	26 3	sylan9eq	$⊢ (((A \in V \land B \in W \land E \in U) \land x = A) \land y = B) \to C = E$
28	25 27	csbied	$⊢ ((A \in V \land B \in W \land E \in U) \land x = A) \to ⦋ B / y ⦌ C = E$
29	24 28	csbied	$⊢ (A \in V \land B \in W \land E \in U) \to ⦋ A / x ⦌ ⦋ B / y ⦌ C = E$
30	29	adantr	$⊢ ((A \in V \land B \in W \land E \in U) \land p = ⟨A, B⟩) \to ⦋ A / x ⦌ ⦋ B / y ⦌ C = E$
31		csbeq1	$⊢ 1^{st} (p) = A \to ⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C = ⦋ A / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C$
32	31	eqeq1d	$⊢ 1^{st} (p) = A \to (⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C = E \leftrightarrow ⦋ A / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C = E)$
33	32	adantl	$⊢ (2^{nd} (p) = B \land 1^{st} (p) = A) \to (⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C = E \leftrightarrow ⦋ A / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C = E)$
34		csbeq1	$⊢ 2^{nd} (p) = B \to ⦋ 2^{nd} (p) / y ⦌ C = ⦋ B / y ⦌ C$
35	34	adantr	$⊢ (2^{nd} (p) = B \land 1^{st} (p) = A) \to ⦋ 2^{nd} (p) / y ⦌ C = ⦋ B / y ⦌ C$
36	35	csbeq2dv	$⊢ (2^{nd} (p) = B \land 1^{st} (p) = A) \to ⦋ A / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C = ⦋ A / x ⦌ ⦋ B / y ⦌ C$
37	36	eqeq1d	$⊢ (2^{nd} (p) = B \land 1^{st} (p) = A) \to (⦋ A / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C = E \leftrightarrow ⦋ A / x ⦌ ⦋ B / y ⦌ C = E)$
38	33 37	bitrd	$⊢ (2^{nd} (p) = B \land 1^{st} (p) = A) \to (⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C = E \leftrightarrow ⦋ A / x ⦌ ⦋ B / y ⦌ C = E)$
39	30 38	syl5ibrcom	$⊢ ((A \in V \land B \in W \land E \in U) \land p = ⟨A, B⟩) \to ((2^{nd} (p) = B \land 1^{st} (p) = A) \to ⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C = E)$
40	16 23 39	mp2and	$⊢ ((A \in V \land B \in W \land E \in U) \land p = ⟨A, B⟩) \to ⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C = E$
41		opex	$⊢ ⟨A, B⟩ \in V$
42	41	a1i	$⊢ (A \in V \land B \in W \land E \in U) \to ⟨A, B⟩ \in V$
43		simp3	$⊢ (A \in V \land B \in W \land E \in U) \to E \in U$
44	40 42 43	fmptsnd	$⊢ (A \in V \land B \in W \land E \in U) \to \{⟨⟨A, B⟩, E⟩\} = (p \in \{⟨A, B⟩\} ⟼ ⦋ 1^{st} (p) / x ⦌ ⦋ 2^{nd} (p) / y ⦌ C)$
45	6 9 44	3eqtr4d	$⊢ (A \in V \land B \in W \land E \in U) \to F = \{⟨⟨A, B⟩, E⟩\}$

Metamath Proof Explorer

Theorem mposn

Proof