Theorem 2arympt

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

	Ref	Expression
Hypothesis	2arympt.f	$$⊢F=\left(x\in \left(X^{\left\{0,1\right\}}\right)⟼x\left(0\right)Ox\left(1\right)\right)$$
Assertion	2arympt	Could not format assertion : No typesetting found for |- ( ( X e. V /\ O : ( X X. X ) --> X ) -> F e. ( 2 -aryF X ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		2arympt.f	$$⊢F=\left(x\in \left(X^{\left\{0,1\right\}}\right)⟼x\left(0\right)Ox\left(1\right)\right)$$
2		simplr	$$⊢\left(\left(X\in V\wedge O:X\times X⟶X\right)\wedge x\in \left(X^{\left\{0,1\right\}}\right)\right)\to O:X\times X⟶X$$
3		elmapi	$$⊢x\in \left(X^{\left\{0,1\right\}}\right)\to x:\left\{0,1\right\}⟶X$$
4		c0ex	$$⊢0\in \mathrm{V}$$
5	4	prid1	$$⊢0\in \left\{0,1\right\}$$
6	5	a1i	$$⊢x\in \left(X^{\left\{0,1\right\}}\right)\to 0\in \left\{0,1\right\}$$
7	3 6	ffvelrnd	$$⊢x\in \left(X^{\left\{0,1\right\}}\right)\to x\left(0\right)\in X$$
8	7	adantl	$$⊢\left(\left(X\in V\wedge O:X\times X⟶X\right)\wedge x\in \left(X^{\left\{0,1\right\}}\right)\right)\to x\left(0\right)\in X$$
9		1ex	$$⊢1\in \mathrm{V}$$
10	9	prid2	$$⊢1\in \left\{0,1\right\}$$
11	10	a1i	$$⊢x\in \left(X^{\left\{0,1\right\}}\right)\to 1\in \left\{0,1\right\}$$
12	3 11	ffvelrnd	$$⊢x\in \left(X^{\left\{0,1\right\}}\right)\to x\left(1\right)\in X$$
13	12	adantl	$$⊢\left(\left(X\in V\wedge O:X\times X⟶X\right)\wedge x\in \left(X^{\left\{0,1\right\}}\right)\right)\to x\left(1\right)\in X$$
14	2 8 13	fovrnd	$$⊢\left(\left(X\in V\wedge O:X\times X⟶X\right)\wedge x\in \left(X^{\left\{0,1\right\}}\right)\right)\to x\left(0\right)Ox\left(1\right)\in X$$
15	14 1	fmptd	$$⊢\left(X\in V\wedge O:X\times X⟶X\right)\to F:X^{\left\{0,1\right\}}⟶X$$
16		2aryfvalel	Could not format ( X e. V -> ( F e. ( 2 -aryF X ) <-> F : ( X ^m { 0 , 1 } ) --> X ) ) : No typesetting found for |- ( X e. V -> ( F e. ( 2 -aryF X ) <-> F : ( X ^m { 0 , 1 } ) --> X ) ) with typecode |-
17	16	adantr	Could not format ( ( X e. V /\ O : ( X X. X ) --> X ) -> ( F e. ( 2 -aryF X ) <-> F : ( X ^m { 0 , 1 } ) --> X ) ) : No typesetting found for |- ( ( X e. V /\ O : ( X X. X ) --> X ) -> ( F e. ( 2 -aryF X ) <-> F : ( X ^m { 0 , 1 } ) --> X ) ) with typecode |-
18	15 17	mpbird	Could not format ( ( X e. V /\ O : ( X X. X ) --> X ) -> F e. ( 2 -aryF X ) ) : No typesetting found for |- ( ( X e. V /\ O : ( X X. X ) --> X ) -> F e. ( 2 -aryF X ) ) with typecode |-