2arymaptf

Description: The mapping of binary (endo)functions is a function into the set of binary operations. (Contributed by AV, 21-May-2024)

		Ref	Expression
	Hypothesis	2arymaptf.h	$⊢ H = (h \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})))$
	Assertion	2arymaptf	$⊢ X \in V \to H : 2 -aryF X ⟶ X^{(X \times X)}$

Proof

Step	Hyp	Ref	Expression
1		2arymaptf.h	$⊢ H = (h \in (2 -aryF X) ⟼ (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})))$
2		simplr	$⊢ ((X \in V \land h \in (2 -aryF X)) \land z \in (X \times X)) \to h \in (2 -aryF X)$
3		xp1st	$⊢ z \in (X \times X) \to 1^{st} (z) \in X$
4	3	adantl	$⊢ ((X \in V \land h \in (2 -aryF X)) \land z \in (X \times X)) \to 1^{st} (z) \in X$
5		xp2nd	$⊢ z \in (X \times X) \to 2^{nd} (z) \in X$
6	5	adantl	$⊢ ((X \in V \land h \in (2 -aryF X)) \land z \in (X \times X)) \to 2^{nd} (z) \in X$
7		fv2arycl	$⊢ (h \in (2 -aryF X) \land 1^{st} (z) \in X \land 2^{nd} (z) \in X) \to h (\{⟨0, 1^{st} (z)⟩, ⟨1, 2^{nd} (z)⟩\}) \in X$
8	2 4 6 7	syl3anc	$⊢ ((X \in V \land h \in (2 -aryF X)) \land z \in (X \times X)) \to h (\{⟨0, 1^{st} (z)⟩, ⟨1, 2^{nd} (z)⟩\}) \in X$
9		vex	$⊢ x \in V$
10		vex	$⊢ y \in V$
11	9 10	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
12	11	opeq2d	$⊢ z = ⟨x, y⟩ \to ⟨0, 1^{st} (z)⟩ = ⟨0, x⟩$
13	9 10	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
14	13	opeq2d	$⊢ z = ⟨x, y⟩ \to ⟨1, 2^{nd} (z)⟩ = ⟨1, y⟩$
15	12 14	preq12d	$⊢ z = ⟨x, y⟩ \to \{⟨0, 1^{st} (z)⟩, ⟨1, 2^{nd} (z)⟩\} = \{⟨0, x⟩, ⟨1, y⟩\}$
16	15	fveq2d	$⊢ z = ⟨x, y⟩ \to h (\{⟨0, 1^{st} (z)⟩, ⟨1, 2^{nd} (z)⟩\}) = h (\{⟨0, x⟩, ⟨1, y⟩\})$
17	16	mpompt	$⊢ (z \in (X \times X) ⟼ h (\{⟨0, 1^{st} (z)⟩, ⟨1, 2^{nd} (z)⟩\})) = (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\}))$
18	17	eqcomi	$⊢ (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})) = (z \in (X \times X) ⟼ h (\{⟨0, 1^{st} (z)⟩, ⟨1, 2^{nd} (z)⟩\}))$
19	8 18	fmptd	$⊢ (X \in V \land h \in (2 -aryF X)) \to (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})) : X \times X ⟶ X$
20		sqxpexg	$⊢ X \in V \to X \times X \in V$
21		elmapg	$⊢ (X \in V \land X \times X \in V) \to ((x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})) \in (X^{(X \times X)}) \leftrightarrow (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})) : X \times X ⟶ X)$
22	20 21	mpdan	$⊢ X \in V \to ((x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})) \in (X^{(X \times X)}) \leftrightarrow (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})) : X \times X ⟶ X)$
23	22	adantr	$⊢ (X \in V \land h \in (2 -aryF X)) \to ((x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})) \in (X^{(X \times X)}) \leftrightarrow (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})) : X \times X ⟶ X)$
24	19 23	mpbird	$⊢ (X \in V \land h \in (2 -aryF X)) \to (x \in X, y \in X ⟼ h (\{⟨0, x⟩, ⟨1, y⟩\})) \in (X^{(X \times X)})$
25	24 1	fmptd	$⊢ X \in V \to H : 2 -aryF X ⟶ X^{(X \times X)}$

Metamath Proof Explorer

Theorem 2arymaptf

Proof