Metamath Proof Explorer

Theorem fourierdlem3

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

Ref Expression
Hypothesis fourierdlem3.1 
|- P = ( m e. NN |-> { p e. ( ( -u _pi [,] _pi ) ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` m ) = _pi ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
Assertion fourierdlem3 
|- ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( ( -u _pi [,] _pi ) ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem3.1 
 |-  P = ( m e. NN |-> { p e. ( ( -u _pi [,] _pi ) ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` m ) = _pi ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
2 oveq2 
 |-  ( m = M -> ( 0 ... m ) = ( 0 ... M ) )
3 2 oveq2d 
 |-  ( m = M -> ( ( -u _pi [,] _pi ) ^m ( 0 ... m ) ) = ( ( -u _pi [,] _pi ) ^m ( 0 ... M ) ) )
4 fveqeq2 
 |-  ( m = M -> ( ( p ` m ) = _pi <-> ( p ` M ) = _pi ) )
5 4 anbi2d 
 |-  ( m = M -> ( ( ( p ` 0 ) = -u _pi /\ ( p ` m ) = _pi ) <-> ( ( p ` 0 ) = -u _pi /\ ( p ` M ) = _pi ) ) )
6 oveq2 
 |-  ( m = M -> ( 0 ..^ m ) = ( 0 ..^ M ) )
7 6 raleqdv 
 |-  ( m = M -> ( A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) )
8 5 7 anbi12d 
 |-  ( m = M -> ( ( ( ( p ` 0 ) = -u _pi /\ ( p ` m ) = _pi ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( p ` 0 ) = -u _pi /\ ( p ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) ) )
9 3 8 rabeqbidv 
 |-  ( m = M -> { p e. ( ( -u _pi [,] _pi ) ^m ( 0 ... m ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` m ) = _pi ) /\ A. i e. ( 0 ..^ m ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } = { p e. ( ( -u _pi [,] _pi ) ^m ( 0 ... M ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
10 ovex 
 |-  ( ( -u _pi [,] _pi ) ^m ( 0 ... M ) ) e. _V
11 10 rabex 
 |-  { p e. ( ( -u _pi [,] _pi ) ^m ( 0 ... M ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } e. _V
12 9 1 11 fvmpt 
 |-  ( M e. NN -> ( P ` M ) = { p e. ( ( -u _pi [,] _pi ) ^m ( 0 ... M ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } )
13 12 eleq2d 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> Q e. { p e. ( ( -u _pi [,] _pi ) ^m ( 0 ... M ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } ) )
14 fveq1 
 |-  ( p = Q -> ( p ` 0 ) = ( Q ` 0 ) )
15 14 eqeq1d 
 |-  ( p = Q -> ( ( p ` 0 ) = -u _pi <-> ( Q ` 0 ) = -u _pi ) )
16 fveq1 
 |-  ( p = Q -> ( p ` M ) = ( Q ` M ) )
17 16 eqeq1d 
 |-  ( p = Q -> ( ( p ` M ) = _pi <-> ( Q ` M ) = _pi ) )
18 15 17 anbi12d 
 |-  ( p = Q -> ( ( ( p ` 0 ) = -u _pi /\ ( p ` M ) = _pi ) <-> ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) ) )
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 -> ( A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) <-> A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) )
23 18 22 anbi12d 
 |-  ( p = Q -> ( ( ( ( p ` 0 ) = -u _pi /\ ( p ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) <-> ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
24 23 elrab 
 |-  ( Q e. { p e. ( ( -u _pi [,] _pi ) ^m ( 0 ... M ) ) | ( ( ( p ` 0 ) = -u _pi /\ ( p ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( p ` i ) < ( p ` ( i + 1 ) ) ) } <-> ( Q e. ( ( -u _pi [,] _pi ) ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) )
25 13 24 bitrdi 
 |-  ( M e. NN -> ( Q e. ( P ` M ) <-> ( Q e. ( ( -u _pi [,] _pi ) ^m ( 0 ... M ) ) /\ ( ( ( Q ` 0 ) = -u _pi /\ ( Q ` M ) = _pi ) /\ A. i e. ( 0 ..^ M ) ( Q ` i ) < ( Q ` ( i + 1 ) ) ) ) ) )