2arympt

Description: 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	2arympt	$⊢ (X \in V \land O : X \times X ⟶ X) \to F \in (2 -aryF X)$

Step	Hyp	Ref	Expression
1		2arympt.f	$⊢ F = (x \in (X^{\{0, 1\}}) ⟼ x (0) O x (1))$
2		simplr	$⊢ ((X \in V \land O : X \times X ⟶ X) \land x \in (X^{\{0, 1\}})) \to O : X \times X ⟶ X$
3		elmapi	$⊢ x \in (X^{\{0, 1\}}) \to x : \{0, 1\} ⟶ X$
4		0elpr01	$⊢ 0 \in \{0, 1\}$
5	4	a1i	$⊢ x \in (X^{\{0, 1\}}) \to 0 \in \{0, 1\}$
6	3 5	ffvelcdmd	$⊢ x \in (X^{\{0, 1\}}) \to x (0) \in X$
7	6	adantl	$⊢ ((X \in V \land O : X \times X ⟶ X) \land x \in (X^{\{0, 1\}})) \to x (0) \in X$
8		1elpr01	$⊢ 1 \in \{0, 1\}$
9	8	a1i	$⊢ x \in (X^{\{0, 1\}}) \to 1 \in \{0, 1\}$
10	3 9	ffvelcdmd	$⊢ x \in (X^{\{0, 1\}}) \to x (1) \in X$
11	10	adantl	$⊢ ((X \in V \land O : X \times X ⟶ X) \land x \in (X^{\{0, 1\}})) \to x (1) \in X$
12	2 7 11	fovcdmd	$⊢ ((X \in V \land O : X \times X ⟶ X) \land x \in (X^{\{0, 1\}})) \to x (0) O x (1) \in X$
13	12 1	fmptd	$⊢ (X \in V \land O : X \times X ⟶ X) \to F : X^{\{0, 1\}} ⟶ X$
14		2aryfvalel	$⊢ X \in V \to (F \in (2 -aryF X) \leftrightarrow F : X^{\{0, 1\}} ⟶ X)$
15	14	adantr	$⊢ (X \in V \land O : X \times X ⟶ X) \to (F \in (2 -aryF X) \leftrightarrow F : X^{\{0, 1\}} ⟶ X)$
16	13 15	mpbird	$⊢ (X \in V \land O : X \times X ⟶ X) \to F \in (2 -aryF X)$

Metamath Proof Explorer