Metamath Proof Explorer

Theorem 2arymptfv

Description: The value of a binary (endo)function in maps-to notation. (Contributed by AV, 20-May-2024)

Ref Expression
Hypothesis 2arympt.f 
|- F = ( x e. ( X ^m { 0 , 1 } ) |-> ( ( x ` 0 ) O ( x ` 1 ) ) )
Assertion 2arymptfv 
|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( F ` { <. 0 , A >. , <. 1 , B >. } ) = ( A O B ) )

Proof

Step Hyp Ref Expression
1 2arympt.f 
 |-  F = ( x e. ( X ^m { 0 , 1 } ) |-> ( ( x ` 0 ) O ( x ` 1 ) ) )
2 fveq1 
 |-  ( x = { <. 0 , A >. , <. 1 , B >. } -> ( x ` 0 ) = ( { <. 0 , A >. , <. 1 , B >. } ` 0 ) )
3 2 adantl 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ x = { <. 0 , A >. , <. 1 , B >. } ) -> ( x ` 0 ) = ( { <. 0 , A >. , <. 1 , B >. } ` 0 ) )
4 c0ex 
 |-  0 e. _V
5 4 a1i 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> 0 e. _V )
6 simp2 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> A e. X )
7 0ne1 
 |-  0 =/= 1
8 7 a1i 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> 0 =/= 1 )
9 5 6 8 3jca 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> ( 0 e. _V /\ A e. X /\ 0 =/= 1 ) )
10 9 adantr 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ x = { <. 0 , A >. , <. 1 , B >. } ) -> ( 0 e. _V /\ A e. X /\ 0 =/= 1 ) )
11 fvpr1g 
 |-  ( ( 0 e. _V /\ A e. X /\ 0 =/= 1 ) -> ( { <. 0 , A >. , <. 1 , B >. } ` 0 ) = A )
12 10 11 syl 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ x = { <. 0 , A >. , <. 1 , B >. } ) -> ( { <. 0 , A >. , <. 1 , B >. } ` 0 ) = A )
13 3 12 eqtrd 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ x = { <. 0 , A >. , <. 1 , B >. } ) -> ( x ` 0 ) = A )
14 fveq1 
 |-  ( x = { <. 0 , A >. , <. 1 , B >. } -> ( x ` 1 ) = ( { <. 0 , A >. , <. 1 , B >. } ` 1 ) )
15 1ex 
 |-  1 e. _V
16 simp3 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> B e. X )
17 fvpr2g 
 |-  ( ( 1 e. _V /\ B e. X /\ 0 =/= 1 ) -> ( { <. 0 , A >. , <. 1 , B >. } ` 1 ) = B )
18 15 16 8 17 mp3an2i 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> ( { <. 0 , A >. , <. 1 , B >. } ` 1 ) = B )
19 14 18 sylan9eqr 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ x = { <. 0 , A >. , <. 1 , B >. } ) -> ( x ` 1 ) = B )
20 13 19 oveq12d 
 |-  ( ( ( X e. V /\ A e. X /\ B e. X ) /\ x = { <. 0 , A >. , <. 1 , B >. } ) -> ( ( x ` 0 ) O ( x ` 1 ) ) = ( A O B ) )
21 simp1 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> X e. V )
22 4 15 7 3pm3.2i 
 |-  ( 0 e. _V /\ 1 e. _V /\ 0 =/= 1 )
23 22 a1i 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> ( 0 e. _V /\ 1 e. _V /\ 0 =/= 1 ) )
24 3simpc 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> ( A e. X /\ B e. X ) )
25 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 } ) )
26 21 23 24 25 syl3anc 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> { <. 0 , A >. , <. 1 , B >. } e. ( X ^m { 0 , 1 } ) )
27 ovexd 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> ( A O B ) e. _V )
28 1 20 26 27 fvmptd2 
 |-  ( ( X e. V /\ A e. X /\ B e. X ) -> ( F ` { <. 0 , A >. , <. 1 , B >. } ) = ( A O B ) )