Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem2 Structured version   Visualization version   GIF version

Theorem fourierdlem2 43986
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
StepHypRef Expression
1 oveq2 7345 . . . . . 6 (𝑚 = 𝑀 → (0...𝑚) = (0...𝑀))
21oveq2d 7353 . . . . 5 (𝑚 = 𝑀 → (ℝ ↑m (0...𝑚)) = (ℝ ↑m (0...𝑀)))
3 fveqeq2 6834 . . . . . . 7 (𝑚 = 𝑀 → ((𝑝𝑚) = 𝐵 ↔ (𝑝𝑀) = 𝐵))
43anbi2d 629 . . . . . 6 (𝑚 = 𝑀 → (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ↔ ((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵)))
5 oveq2 7345 . . . . . . 7 (𝑚 = 𝑀 → (0..^𝑚) = (0..^𝑀))
65raleqdv 3309 . . . . . 6 (𝑚 = 𝑀 → (∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1))))
74, 6anbi12d 631 . . . . 5 (𝑚 = 𝑀 → ((((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))))
82, 7rabeqbidv 3420 . . . 4 (𝑚 = 𝑀 → {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))} = {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
9 fourierdlem2.1 . . . 4 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
10 ovex 7370 . . . . 5 (ℝ ↑m (0...𝑀)) ∈ V
1110rabex 5276 . . . 4 {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))} ∈ V
128, 9, 11fvmpt 6931 . . 3 (𝑀 ∈ ℕ → (𝑃𝑀) = {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
1312eleq2d 2822 . 2 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ 𝑄 ∈ {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}))
14 fveq1 6824 . . . . . 6 (𝑝 = 𝑄 → (𝑝‘0) = (𝑄‘0))
1514eqeq1d 2738 . . . . 5 (𝑝 = 𝑄 → ((𝑝‘0) = 𝐴 ↔ (𝑄‘0) = 𝐴))
16 fveq1 6824 . . . . . 6 (𝑝 = 𝑄 → (𝑝𝑀) = (𝑄𝑀))
1716eqeq1d 2738 . . . . 5 (𝑝 = 𝑄 → ((𝑝𝑀) = 𝐵 ↔ (𝑄𝑀) = 𝐵))
1815, 17anbi12d 631 . . . 4 (𝑝 = 𝑄 → (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ↔ ((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵)))
19 fveq1 6824 . . . . . 6 (𝑝 = 𝑄 → (𝑝𝑖) = (𝑄𝑖))
20 fveq1 6824 . . . . . 6 (𝑝 = 𝑄 → (𝑝‘(𝑖 + 1)) = (𝑄‘(𝑖 + 1)))
2119, 20breq12d 5105 . . . . 5 (𝑝 = 𝑄 → ((𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ (𝑄𝑖) < (𝑄‘(𝑖 + 1))))
2221ralbidv 3170 . . . 4 (𝑝 = 𝑄 → (∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)) ↔ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))
2318, 22anbi12d 631 . . 3 (𝑝 = 𝑄 → ((((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1))) ↔ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
2423elrab 3634 . 2 (𝑄 ∈ {𝑝 ∈ (ℝ ↑m (0...𝑀)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))} ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
2513, 24bitrdi 286 1 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wral 3061  {crab 3403   class class class wbr 5092  cmpt 5175  cfv 6479  (class class class)co 7337  m cmap 8686  cr 10971  0cc0 10972  1c1 10973   + caddc 10975   < clt 11110  cn 12074  ...cfz 13340  ..^cfzo 13483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-mpt 5176  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-iota 6431  df-fun 6481  df-fv 6487  df-ov 7340
This theorem is referenced by:  fourierdlem11  43995  fourierdlem12  43996  fourierdlem13  43997  fourierdlem14  43998  fourierdlem15  43999  fourierdlem34  44018  fourierdlem37  44021  fourierdlem41  44025  fourierdlem48  44031  fourierdlem49  44032  fourierdlem50  44033  fourierdlem54  44037  fourierdlem63  44046  fourierdlem64  44047  fourierdlem65  44048  fourierdlem69  44052  fourierdlem70  44053  fourierdlem72  44055  fourierdlem74  44057  fourierdlem75  44058  fourierdlem76  44059  fourierdlem79  44062  fourierdlem81  44064  fourierdlem85  44068  fourierdlem88  44071  fourierdlem89  44072  fourierdlem90  44073  fourierdlem91  44074  fourierdlem92  44075  fourierdlem93  44076  fourierdlem94  44077  fourierdlem97  44080  fourierdlem102  44085  fourierdlem103  44086  fourierdlem104  44087  fourierdlem111  44094  fourierdlem113  44096  fourierdlem114  44097
  Copyright terms: Public domain W3C validator