Metamath Proof Explorer


Theorem fourierdlem2

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

Ref Expression
Hypothesis fourierdlem2.1 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
Assertion fourierdlem2 ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fourierdlem2.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 ) ) ) ) ) )