Theorem 2arymaptf1

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

	Ref	Expression
Hypothesis	2arymaptf.h	No typesetting found for |- H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
Assertion	2arymaptf1	Could not format assertion : No typesetting found for |- ( X e. V -> H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		2arymaptf.h	Could not format H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : No typesetting found for |- H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
2	1	2arymaptf	Could not format ( X e. V -> H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) ) : No typesetting found for |- ( X e. V -> H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) ) with typecode |-
3	1	2arymaptfv	Could not format ( f e. ( 2 -aryF X ) -> ( H ` f ) = ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : No typesetting found for |- ( f e. ( 2 -aryF X ) -> ( H ` f ) = ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
4	3	ad2antrl	Could not format ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( H ` f ) = ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( H ` f ) = ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
5	1	2arymaptfv	Could not format ( g e. ( 2 -aryF X ) -> ( H ` g ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : No typesetting found for |- ( g e. ( 2 -aryF X ) -> ( H ` g ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
6	5	ad2antll	Could not format ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( H ` g ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( H ` g ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
7	4 6	eqeq12d	Could not format ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) <-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) <-> ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) ) with typecode |-
8		fvex	$$⊢f\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\in \mathrm{V}$$
9	8	rgen2w	$$⊢\forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\in \mathrm{V}$$
10		mpo2eqb	$$⊢\forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\in \mathrm{V}\to \left(\left(x\in X,y\in X⟼f\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)=\left(x\in X,y\in X⟼g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\leftrightarrow \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)$$
11	9 10	mp1i	Could not format ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) <-> A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) <-> A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
12		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 |-
13		2aryfvalel	Could not format ( X e. V -> ( g e. ( 2 -aryF X ) <-> g : ( X ^m { 0 , 1 } ) --> X ) ) : No typesetting found for |- ( X e. V -> ( g e. ( 2 -aryF X ) <-> g : ( X ^m { 0 , 1 } ) --> X ) ) with typecode |-
14	12 13	anbi12d	Could not format ( X e. V -> ( ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) <-> ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) ) ) : No typesetting found for |- ( X e. V -> ( ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) <-> ( f : ( X ^m { 0 , 1 } ) --> X /\ g : ( X ^m { 0 , 1 } ) --> X ) ) ) with typecode |-
15		ffn	$$⊢f:X^{\left\{0,1\right\}}⟶X\to fFn\left(X^{\left\{0,1\right\}}\right)$$
16	15	adantr	$$⊢\left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\to fFn\left(X^{\left\{0,1\right\}}\right)$$
17	16	3ad2ant2	$$⊢\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to fFn\left(X^{\left\{0,1\right\}}\right)$$
18		ffn	$$⊢g:X^{\left\{0,1\right\}}⟶X\to gFn\left(X^{\left\{0,1\right\}}\right)$$
19	18	adantl	$$⊢\left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\to gFn\left(X^{\left\{0,1\right\}}\right)$$
20	19	3ad2ant2	$$⊢\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to gFn\left(X^{\left\{0,1\right\}}\right)$$
21		elmapi	$$⊢z\in \left(X^{\left\{0,1\right\}}\right)\to z:\left\{0,1\right\}⟶X$$
22		0ne1	$$⊢0\ne 1$$
23		c0ex	$$⊢0\in \mathrm{V}$$
24		1ex	$$⊢1\in \mathrm{V}$$
25	23 24	fprb	$$⊢0\ne 1\to \left(z:\left\{0,1\right\}⟶X\leftrightarrow \exists a\in X\exists b\in Xz=\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)$$
26	22 25	ax-mp	$$⊢z:\left\{0,1\right\}⟶X\leftrightarrow \exists a\in X\exists b\in Xz=\left\{⟨0,a⟩,⟨1,b⟩\right\}$$
27	21 26	sylib	$$⊢z\in \left(X^{\left\{0,1\right\}}\right)\to \exists a\in X\exists b\in Xz=\left\{⟨0,a⟩,⟨1,b⟩\right\}$$
28		opeq2	$$⊢x=a\to ⟨0,x⟩=⟨0,a⟩$$
29	28	preq1d	$$⊢x=a\to \left\{⟨0,x⟩,⟨1,y⟩\right\}=\left\{⟨0,a⟩,⟨1,y⟩\right\}$$
30	29	fveq2d	$$⊢x=a\to f\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=f\left(\left\{⟨0,a⟩,⟨1,y⟩\right\}\right)$$
31	29	fveq2d	$$⊢x=a\to g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,y⟩\right\}\right)$$
32	30 31	eqeq12d	$$⊢x=a\to \left(f\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\leftrightarrow f\left(\left\{⟨0,a⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,y⟩\right\}\right)\right)$$
33		opeq2	$$⊢y=b\to ⟨1,y⟩=⟨1,b⟩$$
34	33	preq2d	$$⊢y=b\to \left\{⟨0,a⟩,⟨1,y⟩\right\}=\left\{⟨0,a⟩,⟨1,b⟩\right\}$$
35	34	fveq2d	$$⊢y=b\to f\left(\left\{⟨0,a⟩,⟨1,y⟩\right\}\right)=f\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)$$
36	34	fveq2d	$$⊢y=b\to g\left(\left\{⟨0,a⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)$$
37	35 36	eqeq12d	$$⊢y=b\to \left(f\left(\left\{⟨0,a⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,y⟩\right\}\right)\leftrightarrow f\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)\right)$$
38	32 37	rspc2va	$$⊢\left(\left(a\in X\wedge b\in X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to f\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)$$
39	38	expcom	$$⊢\forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\to \left(\left(a\in X\wedge b\in X\right)\to f\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)\right)$$
40	39	3ad2ant3	$$⊢\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to \left(\left(a\in X\wedge b\in X\right)\to f\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)\right)$$
41	40	com12	$$⊢\left(a\in X\wedge b\in X\right)\to \left(\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to f\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)\right)$$
42	41	adantr	$$⊢\left(\left(a\in X\wedge b\in X\right)\wedge z=\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)\to \left(\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to f\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)\right)$$
43		fveq2	$$⊢z=\left\{⟨0,a⟩,⟨1,b⟩\right\}\to f\left(z\right)=f\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)$$
44		fveq2	$$⊢z=\left\{⟨0,a⟩,⟨1,b⟩\right\}\to g\left(z\right)=g\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)$$
45	43 44	eqeq12d	$$⊢z=\left\{⟨0,a⟩,⟨1,b⟩\right\}\to \left(f\left(z\right)=g\left(z\right)\leftrightarrow f\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)\right)$$
46	45	adantl	$$⊢\left(\left(a\in X\wedge b\in X\right)\wedge z=\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)\to \left(f\left(z\right)=g\left(z\right)\leftrightarrow f\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)=g\left(\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)\right)$$
47	42 46	sylibrd	$$⊢\left(\left(a\in X\wedge b\in X\right)\wedge z=\left\{⟨0,a⟩,⟨1,b⟩\right\}\right)\to \left(\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to f\left(z\right)=g\left(z\right)\right)$$
48	47	ex	$$⊢\left(a\in X\wedge b\in X\right)\to \left(z=\left\{⟨0,a⟩,⟨1,b⟩\right\}\to \left(\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to f\left(z\right)=g\left(z\right)\right)\right)$$
49	48	rexlimivv	$$⊢\exists a\in X\exists b\in Xz=\left\{⟨0,a⟩,⟨1,b⟩\right\}\to \left(\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to f\left(z\right)=g\left(z\right)\right)$$
50	27 49	syl	$$⊢z\in \left(X^{\left\{0,1\right\}}\right)\to \left(\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to f\left(z\right)=g\left(z\right)\right)$$
51	50	impcom	$$⊢\left(\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\wedge z\in \left(X^{\left\{0,1\right\}}\right)\right)\to f\left(z\right)=g\left(z\right)$$
52	17 20 51	eqfnfvd	$$⊢\left(X\in V\wedge \left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\wedge \forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\to f=g$$
53	52	3exp	$$⊢X\in V\to \left(\left(f:X^{\left\{0,1\right\}}⟶X\wedge g:X^{\left\{0,1\right\}}⟶X\right)\to \left(\forall x\in X\forall y\in Xf\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=g\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\to f=g\right)\right)$$
54	14 53	sylbid	Could not format ( X e. V -> ( ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) -> ( A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) -> f = g ) ) ) : No typesetting found for |- ( X e. V -> ( ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) -> ( A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) -> f = g ) ) ) with typecode |-
55	54	imp	Could not format ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) -> f = g ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( A. x e. X A. y e. X ( f ` { <. 0 , x >. , <. 1 , y >. } ) = ( g ` { <. 0 , x >. , <. 1 , y >. } ) -> f = g ) ) with typecode |-
56	11 55	sylbid	Could not format ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> f = g ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( x e. X , y e. X |-> ( f ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( x e. X , y e. X |-> ( g ` { <. 0 , x >. , <. 1 , y >. } ) ) -> f = g ) ) with typecode |-
57	7 56	sylbid	Could not format ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) -> f = g ) ) : No typesetting found for |- ( ( X e. V /\ ( f e. ( 2 -aryF X ) /\ g e. ( 2 -aryF X ) ) ) -> ( ( H ` f ) = ( H ` g ) -> f = g ) ) with typecode |-
58	57	ralrimivva	Could not format ( X e. V -> A. f e. ( 2 -aryF X ) A. g e. ( 2 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) : No typesetting found for |- ( X e. V -> A. f e. ( 2 -aryF X ) A. g e. ( 2 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) with typecode |-
59		dff13	Could not format ( H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) <-> ( H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) /\ A. f e. ( 2 -aryF X ) A. g e. ( 2 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) ) : No typesetting found for |- ( H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) <-> ( H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) /\ A. f e. ( 2 -aryF X ) A. g e. ( 2 -aryF X ) ( ( H ` f ) = ( H ` g ) -> f = g ) ) ) with typecode |-
60	2 58 59	sylanbrc	Could not format ( X e. V -> H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) ) : No typesetting found for |- ( X e. V -> H : ( 2 -aryF X ) -1-1-> ( X ^m ( X X. X ) ) ) with typecode |-