Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ssralv2VD Structured version   Visualization version   GIF version

Theorem ssralv2VD 43240
Description: Quantification restricted to a subclass for two quantifiers. ssralv 4014 for two quantifiers. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ssralv2 42905 is ssralv2VD 43240 without virtual deductions and was automatically derived from ssralv2VD 43240.
1:: (   (𝐴𝐵𝐶𝐷)   ▶   (𝐴𝐵 𝐶𝐷)   )
2:: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥𝐵𝑦𝐷𝜑   )
3:1: (   (𝐴𝐵𝐶𝐷)   ▶   𝐴𝐵   )
4:3,2: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥𝐴𝑦𝐷𝜑   )
5:4: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐷𝜑)   )
6:5: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐷𝜑)   )
7:: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑, 𝑥𝐴   ▶   𝑥𝐴   )
8:7,6: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑, 𝑥𝐴   ▶   𝑦𝐷𝜑   )
9:1: (   (𝐴𝐵𝐶𝐷)   ▶   𝐶𝐷   )
10:9,8: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑, 𝑥𝐴   ▶   𝑦𝐶𝜑   )
11:10: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐶𝜑)   )
12:: ((𝐴𝐵𝐶𝐷) → ∀𝑥(𝐴𝐵𝐶𝐷))
13:: (∀𝑥𝐵𝑦𝐷𝜑 → ∀𝑥𝑥𝐵𝑦𝐷𝜑)
14:12,13,11: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐶𝜑)   )
15:14: (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵 𝑦𝐷𝜑   ▶   𝑥𝐴𝑦𝐶𝜑   )
16:15: (   (𝐴𝐵𝐶𝐷)    ▶   (∀𝑥𝐵𝑦𝐷𝜑 → ∀𝑥𝐴𝑦𝐶𝜑)   )
qed:16: ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷𝜑 → ∀𝑥𝐴𝑦𝐶𝜑))
(Contributed by Alan Sare, 10-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ssralv2VD ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐶   𝑦,𝐶   𝑥,𝐷   𝑦,𝐷
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑦)   𝐵(𝑦)

Proof of Theorem ssralv2VD
StepHypRef Expression
1 ax-5 1914 . . . . 5 ((𝐴𝐵𝐶𝐷) → ∀𝑥(𝐴𝐵𝐶𝐷))
2 hbra1 3283 . . . . 5 (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝑥𝐵𝑦𝐷 𝜑)
3 idn1 42948 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ▶   (𝐴𝐵𝐶𝐷)   )
4 simpr 486 . . . . . . . 8 ((𝐴𝐵𝐶𝐷) → 𝐶𝐷)
53, 4e1a 43001 . . . . . . 7 (   (𝐴𝐵𝐶𝐷)   ▶   𝐶𝐷   )
6 idn3 42989 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑥𝐴   )
7 simpl 484 . . . . . . . . . . . 12 ((𝐴𝐵𝐶𝐷) → 𝐴𝐵)
83, 7e1a 43001 . . . . . . . . . . 11 (   (𝐴𝐵𝐶𝐷)   ▶   𝐴𝐵   )
9 idn2 42987 . . . . . . . . . . 11 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐵𝑦𝐷 𝜑   )
10 ssralv 4014 . . . . . . . . . . 11 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
118, 9, 10e12 43098 . . . . . . . . . 10 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐴𝑦𝐷 𝜑   )
12 df-ral 3062 . . . . . . . . . . 11 (∀𝑥𝐴𝑦𝐷 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
1312biimpi 215 . . . . . . . . . 10 (∀𝑥𝐴𝑦𝐷 𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
1411, 13e2 43005 . . . . . . . . 9 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑)   )
15 sp 2177 . . . . . . . . 9 (∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑) → (𝑥𝐴 → ∀𝑦𝐷 𝜑))
1614, 15e2 43005 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐷 𝜑)   )
17 pm2.27 42 . . . . . . . 8 (𝑥𝐴 → ((𝑥𝐴 → ∀𝑦𝐷 𝜑) → ∀𝑦𝐷 𝜑))
186, 16, 17e32 43132 . . . . . . 7 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑦𝐷 𝜑   )
19 ssralv 4014 . . . . . . 7 (𝐶𝐷 → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
205, 18, 19e13 43122 . . . . . 6 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑦𝐶 𝜑   )
2120in3 42983 . . . . 5 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐶 𝜑)   )
221, 2, 21gen21nv 42994 . . . 4 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑)   )
23 df-ral 3062 . . . . 5 (∀𝑥𝐴𝑦𝐶 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑))
2423biimpri 227 . . . 4 (∀𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑) → ∀𝑥𝐴𝑦𝐶 𝜑)
2522, 24e2 43005 . . 3 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐴𝑦𝐶 𝜑   )
2625in2 42979 . 2 (   (𝐴𝐵𝐶𝐷)   ▶   (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑)   )
2726in1 42945 1 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wal 1540  wcel 2107  wral 3061  wss 3914
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-v 3449  df-in 3921  df-ss 3931  df-vd1 42944  df-vd2 42952  df-vd3 42964
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator