Metamath Proof Explorer

Theorem fv2arycl

Description: Closure of a binary (endo)function. (Contributed by AV, 20-May-2024)

Ref Expression
Assertion fv2arycl 
|- ( ( G e. ( 2 -aryF X ) /\ A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 0 ..^ 2 ) = ( 0 ..^ 2 )
2 1 naryrcl 
 |-  ( G e. ( 2 -aryF X ) -> ( 2 e. NN0 /\ X e. _V ) )
3 2aryfvalel 
 |-  ( X e. _V -> ( G e. ( 2 -aryF X ) <-> G : ( X ^m { 0 , 1 } ) --> X ) )
4 simp2 
 |-  ( ( X e. _V /\ G : ( X ^m { 0 , 1 } ) --> X /\ ( A e. X /\ B e. X ) ) -> G : ( X ^m { 0 , 1 } ) --> X )
5 c0ex 
 |-  0 e. _V
6 1ex 
 |-  1 e. _V
7 0ne1 
 |-  0 =/= 1
8 5 6 7 3pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V /\ 0 =/= 1 )
9 8 a1i 
 |-  ( ( X e. _V /\ G : ( X ^m { 0 , 1 } ) --> X /\ ( A e. X /\ B e. X ) ) -> ( 0 e. _V /\ 1 e. _V /\ 0 =/= 1 ) )
10 fprmappr 
 |-  ( ( X e. _V /\ ( 0 e. _V /\ 1 e. _V /\ 0 =/= 1 ) /\ ( A e. X /\ B e. X ) ) -> { <. 0 , A >. , <. 1 , B >. } e. ( X ^m { 0 , 1 } ) )
11 9 10 syld3an2 
 |-  ( ( X e. _V /\ G : ( X ^m { 0 , 1 } ) --> X /\ ( A e. X /\ B e. X ) ) -> { <. 0 , A >. , <. 1 , B >. } e. ( X ^m { 0 , 1 } ) )
12 4 11 ffvelrnd 
 |-  ( ( X e. _V /\ G : ( X ^m { 0 , 1 } ) --> X /\ ( A e. X /\ B e. X ) ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X )
13 12 3exp 
 |-  ( X e. _V -> ( G : ( X ^m { 0 , 1 } ) --> X -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) )
14 3 13 sylbid 
 |-  ( X e. _V -> ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) )
15 14 adantl 
 |-  ( ( 2 e. NN0 /\ X e. _V ) -> ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) ) )
16 2 15 mpcom 
 |-  ( G e. ( 2 -aryF X ) -> ( ( A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X ) )
17 16 3impib 
 |-  ( ( G e. ( 2 -aryF X ) /\ A e. X /\ B e. X ) -> ( G ` { <. 0 , A >. , <. 1 , B >. } ) e. X )