Metamath Proof Explorer


Theorem resslemOLD

Description: Obsolete version of resseqnbas as of 21-Oct-2024. (Contributed by Mario Carneiro, 26-Nov-2014) (Revised by Mario Carneiro, 2-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses resslemOLD.r R = W 𝑠 A
resslemOLD.e C = E W
resslemOLD.f E = Slot N
resslemOLD.n N
resslemOLD.b 1 < N
Assertion resslemOLD A V C = E R

Proof

Step Hyp Ref Expression
1 resslemOLD.r R = W 𝑠 A
2 resslemOLD.e C = E W
3 resslemOLD.f E = Slot N
4 resslemOLD.n N
5 resslemOLD.b 1 < N
6 eqid Base W = Base W
7 1 6 ressid2 Base W A W V A V R = W
8 7 fveq2d Base W A W V A V E R = E W
9 8 3expib Base W A W V A V E R = E W
10 1 6 ressval2 ¬ Base W A W V A V R = W sSet Base ndx A Base W
11 10 fveq2d ¬ Base W A W V A V E R = E W sSet Base ndx A Base W
12 3 4 ndxid E = Slot E ndx
13 3 4 ndxarg E ndx = N
14 1re 1
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 Base W
20 11 19 eqtr4di ¬ Base W A W V A V E R = E W
21 20 3expib ¬ Base W A W V A V E R = E W
22 9 21 pm2.61i W V A V E R = E W
23 reldmress Rel dom 𝑠
24 23 ovprc1 ¬ W V W 𝑠 A =
25 1 24 syl5eq ¬ W V R =
26 25 fveq2d ¬ W V E R = E
27 3 str0 = E
28 26 27 eqtr4di ¬ W V E R =
29 fvprc ¬ W V E W =
30 28 29 eqtr4d ¬ W V E R = E W
31 30 adantr ¬ W V A V E R = E W
32 22 31 pm2.61ian A V E R = E W
33 2 32 eqtr4id A V C = E R