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 35051
Description: Lemma for mppspst 35054. (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 7405 . 2 {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))} = {π‘₯ ∣ βˆƒπ‘‘βˆƒβ„Žβˆƒπ‘Ž(π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž)))}
2 df-ot 4629 . . . . . . . . . 10 βŸ¨π‘‘, β„Ž, π‘ŽβŸ© = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ©
32eqeq2i 2737 . . . . . . . . 9 (π‘₯ = βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ↔ π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ©)
43biimpri 227 . . . . . . . 8 (π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© β†’ π‘₯ = βŸ¨π‘‘, β„Ž, π‘ŽβŸ©)
54eleq1d 2810 . . . . . . 7 (π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© β†’ (π‘₯ ∈ 𝑃 ↔ βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃))
65biimpar 477 . . . . . 6 ((π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃) β†’ π‘₯ ∈ 𝑃)
76adantrr 714 . . . . 5 ((π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))) β†’ π‘₯ ∈ 𝑃)
87exlimiv 1925 . . . 4 (βˆƒπ‘Ž(π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))) β†’ π‘₯ ∈ 𝑃)
98exlimivv 1927 . . 3 (βˆƒπ‘‘βˆƒβ„Žβˆƒπ‘Ž(π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))) β†’ π‘₯ ∈ 𝑃)
109abssi 4059 . 2 {π‘₯ ∣ βˆƒπ‘‘βˆƒβ„Žβˆƒπ‘Ž(π‘₯ = βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∧ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž)))} βŠ† 𝑃
111, 10eqsstri 4008 1 {βŸ¨βŸ¨π‘‘, β„ŽβŸ©, π‘ŽβŸ© ∣ (βŸ¨π‘‘, β„Ž, π‘ŽβŸ© ∈ 𝑃 ∧ π‘Ž ∈ (π‘‘πΆβ„Ž))} βŠ† 𝑃
Colors of variables: wff setvar class
Syntax hints:   ∧ wa 395   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098  {cab 2701   βŠ† wss 3940  βŸ¨cop 4626  βŸ¨cotp 4628  β€˜cfv 6533  (class class class)co 7401  {coprab 7402  mPreStcmpst 34953  mClscmcls 34957  mPPStcmpps 34958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957  df-ot 4629  df-oprab 7405
This theorem is referenced by:  mppsval  35052  mppspst  35054
  Copyright terms: Public domain W3C validator