Metamath Proof Explorer

Theorem ressval

Description: Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

Ref Expression
Hypotheses ressbas.r 
|- R = ( W |`s A )
ressbas.b 
|- B = ( Base ` W )
Assertion ressval 
|- ( ( W e. X /\ A e. Y ) -> R = if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) )

Proof

Step Hyp Ref Expression
1 ressbas.r 
 |-  R = ( W |`s A )
2 ressbas.b 
 |-  B = ( Base ` W )
3 elex 
 |-  ( W e. X -> W e. _V )
4 elex 
 |-  ( A e. Y -> A e. _V )
5 simpl 
 |-  ( ( W e. _V /\ A e. _V ) -> W e. _V )
6 ovex 
 |-  ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) e. _V
7 ifcl 
 |-  ( ( W e. _V /\ ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) e. _V ) -> if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) e. _V )
8 5 6 7 sylancl 
 |-  ( ( W e. _V /\ A e. _V ) -> if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) e. _V )
9 simpl 
 |-  ( ( w = W /\ a = A ) -> w = W )
10 9 fveq2d 
 |-  ( ( w = W /\ a = A ) -> ( Base ` w ) = ( Base ` W ) )
11 10 2 eqtr4di 
 |-  ( ( w = W /\ a = A ) -> ( Base ` w ) = B )
12 simpr 
 |-  ( ( w = W /\ a = A ) -> a = A )
13 11 12 sseq12d 
 |-  ( ( w = W /\ a = A ) -> ( ( Base ` w ) C_ a <-> B C_ A ) )
14 12 11 ineq12d 
 |-  ( ( w = W /\ a = A ) -> ( a i^i ( Base ` w ) ) = ( A i^i B ) )
15 14 opeq2d 
 |-  ( ( w = W /\ a = A ) -> <. ( Base ` ndx ) , ( a i^i ( Base ` w ) ) >. = <. ( Base ` ndx ) , ( A i^i B ) >. )
16 9 15 oveq12d 
 |-  ( ( w = W /\ a = A ) -> ( w sSet <. ( Base ` ndx ) , ( a i^i ( Base ` w ) ) >. ) = ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )
17 13 9 16 ifbieq12d 
 |-  ( ( w = W /\ a = A ) -> if ( ( Base ` w ) C_ a , w , ( w sSet <. ( Base ` ndx ) , ( a i^i ( Base ` w ) ) >. ) ) = if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) )
18 df-ress 
 |-  |`s = ( w e. _V , a e. _V |-> if ( ( Base ` w ) C_ a , w , ( w sSet <. ( Base ` ndx ) , ( a i^i ( Base ` w ) ) >. ) ) )
19 17 18 ovmpoga 
 |-  ( ( W e. _V /\ A e. _V /\ if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) e. _V ) -> ( W |`s A ) = if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) )
20 8 19 mpd3an3 
 |-  ( ( W e. _V /\ A e. _V ) -> ( W |`s A ) = if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) )
21 3 4 20 syl2an 
 |-  ( ( W e. X /\ A e. Y ) -> ( W |`s A ) = if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) )
22 1 21 syl5eq 
 |-  ( ( W e. X /\ A e. Y ) -> R = if ( B C_ A , W , ( W sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) ) )