Theorem fourierdlem2 46682

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

Hypothesis

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

Assertion

Ref	Expression
fourierdlem2	⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))

Distinct variable groups:   𝐴,𝑚,𝑝   𝐵,𝑚,𝑝   𝑖,𝑀,𝑚,𝑝   𝑄,𝑖,𝑝

Allowed substitution hints:   𝐴(𝑖)   𝐵(𝑖)   𝑃(𝑖,𝑚,𝑝)   𝑄(𝑚)

Proof of Theorem fourierdlem2

Step	Hyp	Ref	Expression
1		oveq2 7408	. . . . . 6 ⊢ (𝑚 = 𝑀 → (0...𝑚) = (0...𝑀))
2	1	oveq2d 7416	. . . . 5 ⊢ (𝑚 = 𝑀 → (ℝ ↑m (0...𝑚)) = (ℝ ↑m (0...𝑀)))
3		fveqeq2 6880	. . . . . . 7 ⊢ (𝑚 = 𝑀 → ((𝑝‘𝑚) = 𝐵 ↔ (𝑝‘𝑀) = 𝐵))
4	3	anbi2d 641	. . . . . 6 ⊢ (𝑚 = 𝑀 → (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ↔ ((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵)))
5		oveq2 7408	. . . . . . 7 ⊢ (𝑚 = 𝑀 → (0..^𝑚) = (0..^𝑀))
6	5	raleqdv 3323	. . . . . 6 ⊢ (𝑚 = 𝑀 → (∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))))
7	4, 6	anbi12d 643	. . . . 5 ⊢ (𝑚 = 𝑀 → ((((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))))
8	2, 7	rabeqbidv 3435	. . . 4 ⊢ (𝑚 = 𝑀 → {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
9		fourierdlem2.1	. . . 4 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
10		ovex 7433	. . . . 5 ⊢ (ℝ ↑m (0...𝑀)) ∈ V
11	10	rabex 5299	. . . 4 ⊢ {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} ∈ V
12	8, 9, 11	fvmpt 6979	. . 3 ⊢ (𝑀 ∈ ℕ → (𝑃‘𝑀) = {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
13	12	eleq2d 2851	. 2 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ 𝑄 ∈ {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}))
14		fveq1 6870	. . . . . 6 ⊢ (𝑝 = 𝑄 → (𝑝‘0) = (𝑄‘0))
15	14	eqeq1d 2767	. . . . 5 ⊢ (𝑝 = 𝑄 → ((𝑝‘0) = 𝐴 ↔ (𝑄‘0) = 𝐴))
16		fveq1 6870	. . . . . 6 ⊢ (𝑝 = 𝑄 → (𝑝‘𝑀) = (𝑄‘𝑀))
17	16	eqeq1d 2767	. . . . 5 ⊢ (𝑝 = 𝑄 → ((𝑝‘𝑀) = 𝐵 ↔ (𝑄‘𝑀) = 𝐵))
18	15, 17	anbi12d 643	. . . 4 ⊢ (𝑝 = 𝑄 → (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ↔ ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵)))
19		fveq1 6870	. . . . . 6 ⊢ (𝑝 = 𝑄 → (𝑝‘𝑖) = (𝑄‘𝑖))
20		fveq1 6870	. . . . . 6 ⊢ (𝑝 = 𝑄 → (𝑝‘(𝑖 + 1)) = (𝑄‘(𝑖 + 1)))
21	19, 20	breq12d 5117	. . . . 5 ⊢ (𝑝 = 𝑄 → ((𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
22	21	ralbidv 3188	. . . 4 ⊢ (𝑝 = 𝑄 → (∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
23	18, 22	anbi12d 643	. . 3 ⊢ (𝑝 = 𝑄 → ((((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
24	23	elrab 3653	. 2 ⊢ (𝑄 ∈ {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))} ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
25	13, 24	bitrdi 290	1 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ∈ wcel 2145  ∀wral 3079  {crab 3417   class class class wbr 5104   ↦ cmpt 5185  ‘cfv 6525  (class class class)co 7400   ↑_m cmap 8812  ℝcr 11087  0cc0 11088  1c1 11089   + caddc 11091   < clt 11231  ℕcn 12221  ...cfz 13523  ..^cfzo 13670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6481  df-fun 6527  df-fv 6533  df-ov 7403

This theorem is referenced by:  fourierdlem11  46691  fourierdlem12  46692  fourierdlem13  46693  fourierdlem14  46694  fourierdlem15  46695  fourierdlem34  46714  fourierdlem37  46717  fourierdlem41  46721  fourierdlem48  46727  fourierdlem49  46728  fourierdlem50  46729  fourierdlem54  46733  fourierdlem63  46742  fourierdlem64  46743  fourierdlem65  46744  fourierdlem69  46748  fourierdlem70  46749  fourierdlem72  46751  fourierdlem74  46753  fourierdlem75  46754  fourierdlem76  46755  fourierdlem79  46758  fourierdlem81  46760  fourierdlem85  46764  fourierdlem88  46767  fourierdlem89  46768  fourierdlem90  46769  fourierdlem91  46770  fourierdlem92  46771  fourierdlem93  46772  fourierdlem94  46773  fourierdlem97  46776  fourierdlem102  46781  fourierdlem103  46782  fourierdlem104  46783  fourierdlem111  46790  fourierdlem113  46792  fourierdlem114  46793