Theorem 2arymaptfv

Description: The value of the mapping of binary (endo)functions. (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	2arymaptfv	Could not format assertion : No typesetting found for |- ( F e. ( 2 -aryF X ) -> ( H ` F ) = ( x e. X , y e. X |-> ( F ` { <. 0 , x >. , <. 1 , y >. } ) ) ) 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		fveq1	$$⊢h=F\to h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)=F\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)$$
3	2	mpoeq3dv	$$⊢h=F\to \left(x\in X,y\in X⟼h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)=\left(x\in X,y\in X⟼F\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)$$
4		eqid	$$⊢\left(0..^2\right)=\left(0..^2\right)$$
5	4	naryrcl	Could not format ( h e. ( 2 -aryF X ) -> ( 2 e. NN0 /\ X e. _V ) ) : No typesetting found for |- ( h e. ( 2 -aryF X ) -> ( 2 e. NN0 /\ X e. _V ) ) with typecode |-
6		mpoexga	$$⊢\left(X\in \mathrm{V}\wedge X\in \mathrm{V}\right)\to \left(x\in X,y\in X⟼h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\in \mathrm{V}$$
7	6	anidms	$$⊢X\in \mathrm{V}\to \left(x\in X,y\in X⟼h\left(\left\{⟨0,x⟩,⟨1,y⟩\right\}\right)\right)\in \mathrm{V}$$
8	5 7	simpl2im	Could not format ( h e. ( 2 -aryF X ) -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) e. _V ) : No typesetting found for |- ( h e. ( 2 -aryF X ) -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) e. _V ) with typecode |-
9	3 1 8	fvmpt3	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 |-