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 ) )