Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  resslem Structured version   Visualization version   Unicode version

Theorem resslem 15260
 Description: Other elements of a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
Hypotheses
Ref Expression
resslem.r s
resslem.e
resslem.f Slot
resslem.n
resslem.b
Assertion
Ref Expression
resslem

Proof of Theorem resslem
StepHypRef Expression
1 resslem.r . . . . . . 7 s
2 eqid 2471 . . . . . . 7
31, 2ressid2 15255 . . . . . 6
43fveq2d 5883 . . . . 5
543expib 1234 . . . 4
61, 2ressval2 15256 . . . . . . 7 sSet
76fveq2d 5883 . . . . . 6 sSet
8 resslem.f . . . . . . . 8 Slot
9 resslem.n . . . . . . . 8
108, 9ndxid 15220 . . . . . . 7 Slot
118, 9ndxarg 15219 . . . . . . . . 9
12 1re 9660 . . . . . . . . . 10
13 resslem.b . . . . . . . . . 10
1412, 13gtneii 9764 . . . . . . . . 9
1511, 14eqnetri 2713 . . . . . . . 8
16 basendx 15251 . . . . . . . 8
1715, 16neeqtrri 2716 . . . . . . 7
1810, 17setsnid 15243 . . . . . 6 sSet
197, 18syl6eqr 2523 . . . . 5
20193expib 1234 . . . 4
215, 20pm2.61i 169 . . 3
22 reldmress 15253 . . . . . . . . 9 s
2322ovprc1 6339 . . . . . . . 8 s
241, 23syl5eq 2517 . . . . . . 7
2524fveq2d 5883 . . . . . 6
268str0 15239 . . . . . 6
2725, 26syl6eqr 2523 . . . . 5
28 fvprc 5873 . . . . 5
2927, 28eqtr4d 2508 . . . 4