2arymptfv

Description: The value of a binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024)

		Ref	Expression
	Hypothesis	2arympt.f	$⊢ F = (x \in (X^{\{0, 1\}}) ⟼ x (0) O x (1))$
	Assertion	2arymptfv	$⊢ (X \in V \land A \in X \land B \in X) \to F (\{⟨0, A⟩, ⟨1, B⟩\}) = A O B$

Proof

Step	Hyp	Ref	Expression
1		2arympt.f	$⊢ F = (x \in (X^{\{0, 1\}}) ⟼ x (0) O x (1))$
2		fveq1	$⊢ x = \{⟨0, A⟩, ⟨1, B⟩\} \to x (0) = \{⟨0, A⟩, ⟨1, B⟩\} (0)$
3	2	adantl	$⊢ ((X \in V \land A \in X \land B \in X) \land x = \{⟨0, A⟩, ⟨1, B⟩\}) \to x (0) = \{⟨0, A⟩, ⟨1, B⟩\} (0)$
4		c0ex	$⊢ 0 \in V$
5	4	a1i	$⊢ (X \in V \land A \in X \land B \in X) \to 0 \in V$
6		simp2	$⊢ (X \in V \land A \in X \land B \in X) \to A \in X$
7		0ne1	$⊢ 0 \neq 1$
8	7	a1i	$⊢ (X \in V \land A \in X \land B \in X) \to 0 \neq 1$
9	5 6 8	3jca	$⊢ (X \in V \land A \in X \land B \in X) \to (0 \in V \land A \in X \land 0 \neq 1)$
10	9	adantr	$⊢ ((X \in V \land A \in X \land B \in X) \land x = \{⟨0, A⟩, ⟨1, B⟩\}) \to (0 \in V \land A \in X \land 0 \neq 1)$
11		fvpr1g	$⊢ (0 \in V \land A \in X \land 0 \neq 1) \to \{⟨0, A⟩, ⟨1, B⟩\} (0) = A$
12	10 11	syl	$⊢ ((X \in V \land A \in X \land B \in X) \land x = \{⟨0, A⟩, ⟨1, B⟩\}) \to \{⟨0, A⟩, ⟨1, B⟩\} (0) = A$
13	3 12	eqtrd	$⊢ ((X \in V \land A \in X \land B \in X) \land x = \{⟨0, A⟩, ⟨1, B⟩\}) \to x (0) = A$
14		fveq1	$⊢ x = \{⟨0, A⟩, ⟨1, B⟩\} \to x (1) = \{⟨0, A⟩, ⟨1, B⟩\} (1)$
15		1ex	$⊢ 1 \in V$
16		simp3	$⊢ (X \in V \land A \in X \land B \in X) \to B \in X$
17		fvpr2g	$⊢ (1 \in V \land B \in X \land 0 \neq 1) \to \{⟨0, A⟩, ⟨1, B⟩\} (1) = B$
18	15 16 8 17	mp3an2i	$⊢ (X \in V \land A \in X \land B \in X) \to \{⟨0, A⟩, ⟨1, B⟩\} (1) = B$
19	14 18	sylan9eqr	$⊢ ((X \in V \land A \in X \land B \in X) \land x = \{⟨0, A⟩, ⟨1, B⟩\}) \to x (1) = B$
20	13 19	oveq12d	$⊢ ((X \in V \land A \in X \land B \in X) \land x = \{⟨0, A⟩, ⟨1, B⟩\}) \to x (0) O x (1) = A O B$
21		simp1	$⊢ (X \in V \land A \in X \land B \in X) \to X \in V$
22	4 15 7	3pm3.2i	$⊢ (0 \in V \land 1 \in V \land 0 \neq 1)$
23	22	a1i	$⊢ (X \in V \land A \in X \land B \in X) \to (0 \in V \land 1 \in V \land 0 \neq 1)$
24		3simpc	$⊢ (X \in V \land A \in X \land B \in X) \to (A \in X \land B \in X)$
25		fprmappr	$⊢ (X \in V \land (0 \in V \land 1 \in V \land 0 \neq 1) \land (A \in X \land B \in X)) \to \{⟨0, A⟩, ⟨1, B⟩\} \in (X^{\{0, 1\}})$
26	21 23 24 25	syl3anc	$⊢ (X \in V \land A \in X \land B \in X) \to \{⟨0, A⟩, ⟨1, B⟩\} \in (X^{\{0, 1\}})$
27		ovexd	$⊢ (X \in V \land A \in X \land B \in X) \to A O B \in V$
28	1 20 26 27	fvmptd2	$⊢ (X \in V \land A \in X \land B \in X) \to F (\{⟨0, A⟩, ⟨1, B⟩\}) = A O B$

Metamath Proof Explorer

Theorem 2arymptfv

Proof