This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fvprif

Description: The value of the pair function at an element of 2o . (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion fvprif 
|- ( ( A e. V /\ B e. W /\ C e. 2o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` C ) = if ( C = (/) , A , B ) )

Proof

Step Hyp Ref Expression
1 fvpr0o 
 |-  ( A e. V -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A )
2 1 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ C e. 2o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A )
3 2 adantr 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = (/) ) -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A )
4 simpr 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = (/) ) -> C = (/) )
5 4 fveq2d 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = (/) ) -> ( { <. (/) , A >. , <. 1o , B >. } ` C ) = ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) )
6 4 iftrued 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = (/) ) -> if ( C = (/) , A , B ) = A )
7 3 5 6 3eqtr4d 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = (/) ) -> ( { <. (/) , A >. , <. 1o , B >. } ` C ) = if ( C = (/) , A , B ) )
8 fvpr1o 
 |-  ( B e. W -> ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) = B )
9 8 3ad2ant2 
 |-  ( ( A e. V /\ B e. W /\ C e. 2o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) = B )
10 9 adantr 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = 1o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) = B )
11 simpr 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = 1o ) -> C = 1o )
12 11 fveq2d 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = 1o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` C ) = ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) )
13 1n0 
 |-  1o =/= (/)
14 13 neii 
 |-  -. 1o = (/)
15 11 eqeq1d 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = 1o ) -> ( C = (/) <-> 1o = (/) ) )
16 14 15 mtbiri 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = 1o ) -> -. C = (/) )
17 16 iffalsed 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = 1o ) -> if ( C = (/) , A , B ) = B )
18 10 12 17 3eqtr4d 
 |-  ( ( ( A e. V /\ B e. W /\ C e. 2o ) /\ C = 1o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` C ) = if ( C = (/) , A , B ) )
19 elpri 
 |-  ( C e. { (/) , 1o } -> ( C = (/) \/ C = 1o ) )
20 df2o3 
 |-  2o = { (/) , 1o }
21 19 20 eleq2s 
 |-  ( C e. 2o -> ( C = (/) \/ C = 1o ) )
22 21 3ad2ant3 
 |-  ( ( A e. V /\ B e. W /\ C e. 2o ) -> ( C = (/) \/ C = 1o ) )
23 7 18 22 mpjaodan 
 |-  ( ( A e. V /\ B e. W /\ C e. 2o ) -> ( { <. (/) , A >. , <. 1o , B >. } ` C ) = if ( C = (/) , A , B ) )