Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mppspstlem Structured version   Visualization version   GIF version

Theorem mppspstlem 34857
Description: Lemma for mppspst 34860. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mppsval.p 𝑃 = (mPreStβ€˜π‘‡)
mppsval.j 𝐽 = (mPPStβ€˜π‘‡)
mppsval.c 𝐢 = (mClsβ€˜π‘‡)
Assertion
Ref Expression
mppspstlem {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))} βŠ† 𝑃
Distinct variable groups:   π‘Ž,𝑑,β„Ž,𝐢   𝑃,π‘Ž,𝑑,β„Ž   𝑇,π‘Ž,𝑑,β„Ž
Allowed substitution hints:   𝐽(β„Ž,π‘Ž,𝑑)

Proof of Theorem mppspstlem
Dummy variable π‘₯ is distinct from all other variables.
StepHypRef Expression
1 df-oprab 7416 . 2 {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))} = {π‘₯ ∣ βˆƒπ‘‘βˆƒβ„Žβˆƒπ‘Ž(π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž)))}
2 df-ot 4638 . . . . . . . . . 10 βŸ¨π‘‘, β„Ž, π‘ŽβŸ© = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ©
32eqeq2i 2744 . . . . . . . . 9 (π‘₯ = βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ↔ π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ©)
43biimpri 227 . . . . . . . 8 (π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© β†’ π‘₯ = βŸ¨π‘‘, β„Ž, π‘ŽβŸ©)
54eleq1d 2817 . . . . . . 7 (π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© β†’ (π‘₯ ∈ 𝑃 ↔ βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃))
65biimpar 477 . . . . . 6 ((π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃) β†’ π‘₯ ∈ 𝑃)
76adantrr 714 . . . . 5 ((π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))) β†’ π‘₯ ∈ 𝑃)
87exlimiv 1932 . . . 4 (βˆƒπ‘Ž(π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))) β†’ π‘₯ ∈ 𝑃)
98exlimivv 1934 . . 3 (βˆƒπ‘‘βˆƒβ„Žβˆƒπ‘Ž(π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))) β†’ π‘₯ ∈ 𝑃)
109abssi 4068 . 2 {π‘₯ ∣ βˆƒπ‘‘βˆƒβ„Žβˆƒπ‘Ž(π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž)))} βŠ† 𝑃
111, 10eqsstri 4017 1 {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))} βŠ† 𝑃
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 395   = wceq 1540  βˆƒwex 1780   ∈ wcel 2105  {cab 2708   βŠ† wss 3949  βŸ¨cop 4635  βŸ¨cotp 4637  β€˜cfv 6544  (class class class)co 7412  {coprab 7413  mPreStcmpst 34759  mClscmcls 34763  mPPStcmpps 34764
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-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3956  df-ss 3966  df-ot 4638  df-oprab 7416
This theorem is referenced by:  mppsval  34858  mppspst  34860
  Copyright terms: Public domain W3C validator