Metamath Proof Explorer

Theorem fourierdlem3

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

Ref Expression
Hypothesis fourierdlem3.1 ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
Assertion fourierdlem3 ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem3.1 ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
2 oveq2 ⊢ ( 𝑚 = 𝑀 → ( 0 ... 𝑚 ) = ( 0 ... 𝑀 ) )
3 2 oveq2d ⊢ ( 𝑚 = 𝑀 → ( ( - π [,] π ) ↑m ( 0 ... 𝑚 ) ) = ( ( - π [,] π ) ↑m ( 0 ... 𝑀 ) ) )
4 fveqeq2 ⊢ ( 𝑚 = 𝑀 → ( ( 𝑝 ‘ 𝑚 ) = π ↔ ( 𝑝 ‘ 𝑀 ) = π ) )
5 4 anbi2d ⊢ ( 𝑚 = 𝑀 → ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ↔ ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑀 ) = π ) ) )
6 oveq2 ⊢ ( 𝑚 = 𝑀 → ( 0 ..^ 𝑚 ) = ( 0 ..^ 𝑀 ) )
7 6 raleqdv ⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) )
8 5 7 anbi12d ⊢ ( 𝑚 = 𝑀 → ( ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ) )
9 3 8 rabeqbidv ⊢ ( 𝑚 = 𝑀 → { 𝑝 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑚 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } = { 𝑝 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑀 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
10 ovex ⊢ ( ( - π [,] π ) ↑m ( 0 ... 𝑀 ) ) ∈ V
11 10 rabex ⊢ { 𝑝 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑀 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ∈ V
12 9 1 11 fvmpt ⊢ ( 𝑀 ∈ ℕ → ( 𝑃 ‘ 𝑀 ) = { 𝑝 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑀 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
13 12 eleq2d ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ 𝑄 ∈ { 𝑝 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑀 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) )
14 fveq1 ⊢ ( 𝑝 = 𝑄 → ( 𝑝 ‘ 0 ) = ( 𝑄 ‘ 0 ) )
15 14 eqeq1d ⊢ ( 𝑝 = 𝑄 → ( ( 𝑝 ‘ 0 ) = - π ↔ ( 𝑄 ‘ 0 ) = - π ) )
16 fveq1 ⊢ ( 𝑝 = 𝑄 → ( 𝑝 ‘ 𝑀 ) = ( 𝑄 ‘ 𝑀 ) )
17 16 eqeq1d ⊢ ( 𝑝 = 𝑄 → ( ( 𝑝 ‘ 𝑀 ) = π ↔ ( 𝑄 ‘ 𝑀 ) = π ) )
18 15 17 anbi12d ⊢ ( 𝑝 = 𝑄 → ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑀 ) = π ) ↔ ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ) )
19 fveq1 ⊢ ( 𝑝 = 𝑄 → ( 𝑝 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑖 ) )
20 fveq1 ⊢ ( 𝑝 = 𝑄 → ( 𝑝 ‘ ( 𝑖 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
21 19 20 breq12d ⊢ ( 𝑝 = 𝑄 → ( ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
22 21 ralbidv ⊢ ( 𝑝 = 𝑄 → ( ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ↔ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
23 18 22 anbi12d ⊢ ( 𝑝 = 𝑄 → ( ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) ↔ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
24 23 elrab ⊢ ( 𝑄 ∈ { 𝑝 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑀 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ↔ ( 𝑄 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
25 13 24 bitrdi ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ( - π [,] π ) ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )