Metamath Proof Explorer


Theorem fourierdlem2

Description: Membership in a partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis fourierdlem2.1 P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
Assertion fourierdlem2 M Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1

Proof

Step Hyp Ref Expression
1 fourierdlem2.1 P = m p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1
2 oveq2 m = M 0 m = 0 M
3 2 oveq2d m = M 0 m = 0 M
4 fveqeq2 m = M p m = B p M = B
5 4 anbi2d m = M p 0 = A p m = B p 0 = A p M = B
6 oveq2 m = M 0 ..^ m = 0 ..^ M
7 6 raleqdv m = M i 0 ..^ m p i < p i + 1 i 0 ..^ M p i < p i + 1
8 5 7 anbi12d m = M p 0 = A p m = B i 0 ..^ m p i < p i + 1 p 0 = A p M = B i 0 ..^ M p i < p i + 1
9 3 8 rabeqbidv m = M p 0 m | p 0 = A p m = B i 0 ..^ m p i < p i + 1 = p 0 M | p 0 = A p M = B i 0 ..^ M p i < p i + 1
10 ovex 0 M V
11 10 rabex p 0 M | p 0 = A p M = B i 0 ..^ M p i < p i + 1 V
12 9 1 11 fvmpt M P M = p 0 M | p 0 = A p M = B i 0 ..^ M p i < p i + 1
13 12 eleq2d M Q P M Q p 0 M | p 0 = A p M = B i 0 ..^ M p i < p i + 1
14 fveq1 p = Q p 0 = Q 0
15 14 eqeq1d p = Q p 0 = A Q 0 = A
16 fveq1 p = Q p M = Q M
17 16 eqeq1d p = Q p M = B Q M = B
18 15 17 anbi12d p = Q p 0 = A p M = B Q 0 = A Q M = B
19 fveq1 p = Q p i = Q i
20 fveq1 p = Q p i + 1 = Q i + 1
21 19 20 breq12d p = Q p i < p i + 1 Q i < Q i + 1
22 21 ralbidv p = Q i 0 ..^ M p i < p i + 1 i 0 ..^ M Q i < Q i + 1
23 18 22 anbi12d p = Q p 0 = A p M = B i 0 ..^ M p i < p i + 1 Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
24 23 elrab Q p 0 M | p 0 = A p M = B i 0 ..^ M p i < p i + 1 Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1
25 13 24 bitrdi M Q P M Q 0 M Q 0 = A Q M = B i 0 ..^ M Q i < Q i + 1