Metamath Proof Explorer

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 
|- H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) )
Assertion 2arymaptf 
|- ( X e. V -> H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) )

Proof

Step Hyp Ref Expression
1 2arymaptf.h 
 |-  H = ( h e. ( 2 -aryF X ) |-> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) )
2 simplr 
 |-  ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> h e. ( 2 -aryF X ) )
3 xp1st 
 |-  ( z e. ( X X. X ) -> ( 1st ` z ) e. X )
4 3 adantl 
 |-  ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> ( 1st ` z ) e. X )
5 xp2nd 
 |-  ( z e. ( X X. X ) -> ( 2nd ` z ) e. X )
6 5 adantl 
 |-  ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> ( 2nd ` z ) e. X )
7 fv2arycl 
 |-  ( ( h e. ( 2 -aryF X ) /\ ( 1st ` z ) e. X /\ ( 2nd ` z ) e. X ) -> ( h ` { <. 0 , ( 1st ` z ) >. , <. 1 , ( 2nd ` z ) >. } ) e. X )
8 2 4 6 7 syl3anc 
 |-  ( ( ( X e. V /\ h e. ( 2 -aryF X ) ) /\ z e. ( X X. X ) ) -> ( h ` { <. 0 , ( 1st ` z ) >. , <. 1 , ( 2nd ` z ) >. } ) e. X )
9 vex 
 |-  x e. _V
10 vex 
 |-  y e. _V
11 9 10 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
12 11 opeq2d 
 |-  ( z = <. x , y >. -> <. 0 , ( 1st ` z ) >. = <. 0 , x >. )
13 9 10 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
14 13 opeq2d 
 |-  ( z = <. x , y >. -> <. 1 , ( 2nd ` z ) >. = <. 1 , y >. )
15 12 14 preq12d 
 |-  ( z = <. x , y >. -> { <. 0 , ( 1st ` z ) >. , <. 1 , ( 2nd ` z ) >. } = { <. 0 , x >. , <. 1 , y >. } )
16 15 fveq2d 
 |-  ( z = <. x , y >. -> ( h ` { <. 0 , ( 1st ` z ) >. , <. 1 , ( 2nd ` z ) >. } ) = ( h ` { <. 0 , x >. , <. 1 , y >. } ) )
17 16 mpompt 
 |-  ( z e. ( X X. X ) |-> ( h ` { <. 0 , ( 1st ` z ) >. , <. 1 , ( 2nd ` z ) >. } ) ) = ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) )
18 17 eqcomi 
 |-  ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) = ( z e. ( X X. X ) |-> ( h ` { <. 0 , ( 1st ` z ) >. , <. 1 , ( 2nd ` z ) >. } ) )
19 8 18 fmptd 
 |-  ( ( X e. V /\ h e. ( 2 -aryF X ) ) -> ( x e. X , y e. X |-> ( h ` { <. 0 , x >. , <. 1 , y >. } ) ) : ( X X. X ) --> X )
20 sqxpexg 
 |-  ( X e. V -> ( X X. X ) e. _V )
21 elmapg 
 |-  ( ( X e. V /\ ( X X. X ) e. _V ) -> ( ( 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 ) )
22 20 21 mpdan 
 |-  ( X e. V -> ( ( 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 ) )
23 22 adantr 
 |-  ( ( 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 ) )
24 19 23 mpbird 
 |-  ( ( 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 ) ) )
25 24 1 fmptd 
 |-  ( X e. V -> H : ( 2 -aryF X ) --> ( X ^m ( X X. X ) ) )