Metamath Proof Explorer

Theorem resslem

Description: Other elements of a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014) (Revised by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses resslem.r 
|- R = ( W |`s A )
resslem.e 
|- C = ( E ` W )
resslem.f 
|- E = Slot N
resslem.n 
|- N e. NN
resslem.b 
|- 1 < N
Assertion resslem 
|- ( A e. V -> C = ( E ` R ) )

Proof

Step Hyp Ref Expression
1 resslem.r 
 |-  R = ( W |`s A )
2 resslem.e 
 |-  C = ( E ` W )
3 resslem.f 
 |-  E = Slot N
4 resslem.n 
 |-  N e. NN
5 resslem.b 
 |-  1 < N
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 1 6 ressid2 
 |-  ( ( ( Base ` W ) C_ A /\ W e. _V /\ A e. V ) -> R = W )
8 7 fveq2d 
 |-  ( ( ( Base ` W ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
9 8 3expib 
 |-  ( ( Base ` W ) C_ A -> ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) ) )
10 1 6 ressval2 
 |-  ( ( -. ( Base ` W ) C_ A /\ W e. _V /\ A e. V ) -> R = ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) )
11 10 fveq2d 
 |-  ( ( -. ( Base ` W ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) ) )
12 3 4 ndxid 
 |-  E = Slot ( E ` ndx )
13 3 4 ndxarg 
 |-  ( E ` ndx ) = N
14 1re 
 |-  1 e. RR
15 14 5 gtneii 
 |-  N =/= 1
16 13 15 eqnetri 
 |-  ( E ` ndx ) =/= 1
17 basendx 
 |-  ( Base ` ndx ) = 1
18 16 17 neeqtrri 
 |-  ( E ` ndx ) =/= ( Base ` ndx )
19 12 18 setsnid 
 |-  ( E ` W ) = ( E ` ( W sSet <. ( Base ` ndx ) , ( A i^i ( Base ` W ) ) >. ) )
20 11 19 eqtr4di 
 |-  ( ( -. ( Base ` W ) C_ A /\ W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
21 20 3expib 
 |-  ( -. ( Base ` W ) C_ A -> ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) ) )
22 9 21 pm2.61i 
 |-  ( ( W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
23 reldmress 
 |-  Rel dom |`s
24 23 ovprc1 
 |-  ( -. W e. _V -> ( W |`s A ) = (/) )
25 1 24 syl5eq 
 |-  ( -. W e. _V -> R = (/) )
26 25 fveq2d 
 |-  ( -. W e. _V -> ( E ` R ) = ( E ` (/) ) )
27 3 str0 
 |-  (/) = ( E ` (/) )
28 26 27 eqtr4di 
 |-  ( -. W e. _V -> ( E ` R ) = (/) )
29 fvprc 
 |-  ( -. W e. _V -> ( E ` W ) = (/) )
30 28 29 eqtr4d 
 |-  ( -. W e. _V -> ( E ` R ) = ( E ` W ) )
31 30 adantr 
 |-  ( ( -. W e. _V /\ A e. V ) -> ( E ` R ) = ( E ` W ) )
32 22 31 pm2.61ian 
 |-  ( A e. V -> ( E ` R ) = ( E ` W ) )
33 2 32 eqtr4id 
 |-  ( A e. V -> C = ( E ` R ) )