Theorem 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	No typesetting found for |- H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) ) with typecode |-
Assertion	2arymaptf	Could not format assertion : No typesetting found for |- ( X e. V -> H : ( 2 -aryF X ) --> ( 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		simplr	Could not format ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> h e. ( 2 -aryF X ) ) : No typesetting found for |- ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> h e. ( 2 -aryF X ) ) with typecode |-
3		xp1st	$$⊢z\in \left(X\times X\right)\to 1^{st}\left(z\right)\in X$$
4	3	adantl	Could not format ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> ( 1st ` z ) e. X ) : No typesetting found for |- ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> ( 1st ` z ) e. X ) with typecode |-
5		xp2nd	$$⊢z\in \left(X\times X\right)\to 2^{nd}\left(z\right)\in X$$
6	5	adantl	Could not format ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> ( 2nd ` z ) e. X ) : No typesetting found for |- ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> ( 2nd ` z ) e. X ) with typecode |-
7		fv2arycl	Could not format ( ( h e. ( 2 -aryF X ) /\ ( 1st ` z ) e. X /\ ( 2nd ` z ) e. X ) -> ( h ` { <. 0 , ( 1st ` z ) >. , <. 1 , ( 2nd ` z ) >. } ) e. X ) : No typesetting found for |- ( ( h e. ( 2 -aryF X ) /\ ( 1st ` z ) e. X /\ ( 2nd ` z ) e. X ) -> ( h ` { <. 0 , ( 1st ` z ) >. , <. 1 , ( 2nd ` z ) >. } ) e. X ) with typecode |-
8	2 4 6 7	syl3anc	Could not format ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> ( h ` { <. 0 , ( 1st ` z ) >. , <. 1 , ( 2nd ` z ) >. } ) e. X ) : No typesetting found for |- ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> ( h ` { <. 0 , ( 1st ` z ) >. , <. 1 , ( 2nd ` z ) >. } ) e. X ) with typecode |-
9		vex	$$⊢x\in \mathrm{V}$$
10		vex	$$⊢y\in \mathrm{V}$$
11	9 10	op1std	$$⊢z=⟨x,y⟩\to 1^{st}\left(z\right)=x$$
12	11	opeq2d	$$⊢z=⟨x,y⟩\to ⟨0,1^{st}\left(z\right)⟩=⟨0,x⟩$$
13	9 10	op2ndd	$$⊢z=⟨x,y⟩\to 2^{nd}\left(z\right)=y$$
14	13	opeq2d	$$⊢z=⟨x,y⟩\to ⟨1,2^{nd}\left(z\right)⟩=⟨1,y⟩$$
15	12 14	preq12d	$$⊢z=⟨x,y⟩\to \left\{⟨0,1^{st}\left(z\right)⟩,⟨1,2^{nd}\left(z\right)⟩\right\}=\left\{⟨0,x⟩,⟨1,y⟩\right\}$$
16	15	fveq2d	$$⊢z=⟨x,y⟩\to h\left(\left\{⟨0,1^{st}\left(z\right)⟩,⟨1,2^{nd}\left(z\right)⟩\right\}\right)=h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)$$
17	16	mpompt	$$⊢\left(z\in \left(X\times X\right)⟼h\left(\left\{⟨0,1^{st}\left(z\right)⟩,⟨1,2^{nd}\left(z\right)⟩\right\}\right)\right)=\left(x\in X,y\in X⟼h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)$$
18	17	eqcomi	$$⊢\left(x\in X,y\in X⟼h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)=\left(z\in \left(X\times X\right)⟼h\left(\left\{⟨0,1^{st}\left(z\right)⟩,⟨1,2^{nd}\left(z\right)⟩\right\}\right)\right)$$
19	8 18	fmptd	Could not format ( ( X e. V /\ h e. ( 2 -aryF X ) ) -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) : ( X X. X ) --> X ) : No typesetting found for |- ( ( X e. V /\ h e. ( 2 -aryF X ) ) -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) : ( X X. X ) --> X ) with typecode |-
20		sqxpexg	$$⊢X\in V\to X\times X\in \mathrm{V}$$
21		elmapg	$$⊢\left(X\in V\wedge X\times X\in \mathrm{V}\right)\to \left(\left(x\in X,y\in X⟼h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\in \left(X^{\left(X\times X\right)}\right)\leftrightarrow \left(x\in X,y\in X⟼h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right):X\times X⟶X\right)$$
22	20 21	mpdan	$$⊢X\in V\to \left(\left(x\in X,y\in X⟼h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\in \left(X^{\left(X\times X\right)}\right)\leftrightarrow \left(x\in X,y\in X⟼h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right):X\times X⟶X\right)$$
23	22	adantr	Could not format ( ( X e. V /\ h e. ( 2 -aryF X ) ) -> ( ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) e. ( X ^m ( X X. X ) ) <-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) : ( X X. X ) --> X ) ) : No typesetting found for |- ( ( X e. V /\ h e. ( 2 -aryF X ) ) -> ( ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) e. ( X ^m ( X X. X ) ) <-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) : ( X X. X ) --> X ) ) with typecode |-
24	19 23	mpbird	Could not format ( ( X e. V /\ h e. ( 2 -aryF X ) ) -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) e. ( X ^m ( X X. X ) ) ) : No typesetting found for |- ( ( X e. V /\ h e. ( 2 -aryF X ) ) -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) e. ( X ^m ( X X. X ) ) ) with typecode |-
25	24 1	fmptd	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 |-