Theorem 2arympt

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

	Ref	Expression
Hypothesis	2arympt.f	|- F = ( x e. ( X ^m { 0 , 1 } ) |-> ( ( x ` 0 ) O ( x ` 1 ) ) )
Assertion	2arympt	|- ( ( X e. V /\ O : ( X X. X ) --> X ) -> F e. ( 2 -aryF X ) )

Proof

Step	Hyp	Ref	Expression
1		2arympt.f	|- F = ( x e. ( X ^m { 0 , 1 } ) |-> ( ( x ` 0 ) O ( x ` 1 ) ) )
2		simplr	|- ( ( ( X e. V /\ O : ( X X. X ) --> X ) /\ x e. ( X ^m { 0 , 1 } ) ) -> O : ( X X. X ) --> X )
3		elmapi	|- ( x e. ( X ^m { 0 , 1 } ) -> x : { 0 , 1 } --> X )
4		c0ex	|- 0 e. _V
5	4	prid1	|- 0 e. { 0 , 1 }
6	5	a1i	|- ( x e. ( X ^m { 0 , 1 } ) -> 0 e. { 0 , 1 } )
7	3 6	ffvelrnd	|- ( x e. ( X ^m { 0 , 1 } ) -> ( x ` 0 ) e. X )
8	7	adantl	|- ( ( ( X e. V /\ O : ( X X. X ) --> X ) /\ x e. ( X ^m { 0 , 1 } ) ) -> ( x ` 0 ) e. X )
9		1ex	|- 1 e. _V
10	9	prid2	|- 1 e. { 0 , 1 }
11	10	a1i	|- ( x e. ( X ^m { 0 , 1 } ) -> 1 e. { 0 , 1 } )
12	3 11	ffvelrnd	|- ( x e. ( X ^m { 0 , 1 } ) -> ( x ` 1 ) e. X )
13	12	adantl	|- ( ( ( X e. V /\ O : ( X X. X ) --> X ) /\ x e. ( X ^m { 0 , 1 } ) ) -> ( x ` 1 ) e. X )
14	2 8 13	fovrnd	|- ( ( ( X e. V /\ O : ( X X. X ) --> X ) /\ x e. ( X ^m { 0 , 1 } ) ) -> ( ( x ` 0 ) O ( x ` 1 ) ) e. X )
15	14 1	fmptd	|- ( ( X e. V /\ O : ( X X. X ) --> X ) -> F : ( X ^m { 0 , 1 } ) --> X )
16		2aryfvalel	|- ( X e. V -> ( F e. ( 2 -aryF X ) <-> F : ( X ^m { 0 , 1 } ) --> X ) )
17	16	adantr	|- ( ( X e. V /\ O : ( X X. X ) --> X ) -> ( F e. ( 2 -aryF X ) <-> F : ( X ^m { 0 , 1 } ) --> X ) )
18	15 17	mpbird	|- ( ( X e. V /\ O : ( X X. X ) --> X ) -> F e. ( 2 -aryF X ) )