Metamath Proof Explorer

Theorem xpsfeq

Description: A function on 2o is determined by its values at zero and one. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion xpsfeq 
|- ( G Fn 2o -> { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } = G )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( G ` (/) ) e. _V
2 fvex 
 |-  ( G ` 1o ) e. _V
3 fnpr2o 
 |-  ( ( ( G ` (/) ) e. _V /\ ( G ` 1o ) e. _V ) -> { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } Fn 2o )
4 1 2 3 mp2an 
 |-  { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } Fn 2o
5 4 a1i 
 |-  ( G Fn 2o -> { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } Fn 2o )
6 id 
 |-  ( G Fn 2o -> G Fn 2o )
7 elpri 
 |-  ( k e. { (/) , 1o } -> ( k = (/) \/ k = 1o ) )
8 df2o3 
 |-  2o = { (/) , 1o }
9 7 8 eleq2s 
 |-  ( k e. 2o -> ( k = (/) \/ k = 1o ) )
10 fvpr0o 
 |-  ( ( G ` (/) ) e. _V -> ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` (/) ) = ( G ` (/) ) )
11 1 10 ax-mp 
 |-  ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` (/) ) = ( G ` (/) )
12 fveq2 
 |-  ( k = (/) -> ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` k ) = ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` (/) ) )
13 fveq2 
 |-  ( k = (/) -> ( G ` k ) = ( G ` (/) ) )
14 11 12 13 3eqtr4a 
 |-  ( k = (/) -> ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` k ) = ( G ` k ) )
15 fvpr1o 
 |-  ( ( G ` 1o ) e. _V -> ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` 1o ) = ( G ` 1o ) )
16 2 15 ax-mp 
 |-  ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` 1o ) = ( G ` 1o )
17 fveq2 
 |-  ( k = 1o -> ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` k ) = ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` 1o ) )
18 fveq2 
 |-  ( k = 1o -> ( G ` k ) = ( G ` 1o ) )
19 16 17 18 3eqtr4a 
 |-  ( k = 1o -> ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` k ) = ( G ` k ) )
20 14 19 jaoi 
 |-  ( ( k = (/) \/ k = 1o ) -> ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` k ) = ( G ` k ) )
21 9 20 syl 
 |-  ( k e. 2o -> ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` k ) = ( G ` k ) )
22 21 adantl 
 |-  ( ( G Fn 2o /\ k e. 2o ) -> ( { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } ` k ) = ( G ` k ) )
23 5 6 22 eqfnfvd 
 |-  ( G Fn 2o -> { <. (/) , ( G ` (/) ) >. , <. 1o , ( G ` 1o ) >. } = G )