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

Theorem resslem 13527
 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 2438 . . . . . . 7
31, 2ressid2 13522 . . . . . 6
43fveq2d 5735 . . . . 5
543expib 1157 . . . 4
61, 2ressval2 13523 . . . . . . 7 sSet
76fveq2d 5735 . . . . . 6 sSet
8 resslem.f . . . . . . . 8 Slot
9 resslem.n . . . . . . . 8
108, 9ndxid 13495 . . . . . . 7 Slot
118, 9ndxarg 13494 . . . . . . . . 9
12 1re 9095 . . . . . . . . . 10
13 resslem.b . . . . . . . . . 10
1412, 13gtneii 9190 . . . . . . . . 9
1511, 14eqnetri 2620 . . . . . . . 8
16 basendx 13519 . . . . . . . 8
1715, 16neeqtrri 2626 . . . . . . 7
1810, 17setsnid 13514 . . . . . 6 sSet
197, 18syl6eqr 2488 . . . . 5
20193expib 1157 . . . 4
215, 20pm2.61i 159 . . 3
22 reldmress 13520 . . . . . . . . 9 s
2322ovprc1 6112 . . . . . . . 8 s
241, 23syl5eq 2482 . . . . . . 7
2524fveq2d 5735 . . . . . 6
268str0 13510 . . . . . 6
2725, 26syl6eqr 2488 . . . . 5
28 fvprc 5725 . . . . 5
2927, 28eqtr4d 2473 . . . 4