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