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 43709
Description: Quantification restricted to a subclass for two quantifiers. ssralv 4050 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 43374 is ssralv2VD 43709 without virtual deductions and was automatically derived from ssralv2VD 43709.
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 1913 . . . . 5 ((𝐴𝐵𝐶𝐷) → ∀𝑥(𝐴𝐵𝐶𝐷))
2 hbra1 3298 . . . . 5 (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝑥𝐵𝑦𝐷 𝜑)
3 idn1 43417 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ▶   (𝐴𝐵𝐶𝐷)   )
4 simpr 485 . . . . . . . 8 ((𝐴𝐵𝐶𝐷) → 𝐶𝐷)
53, 4e1a 43470 . . . . . . 7 (   (𝐴𝐵𝐶𝐷)   ▶   𝐶𝐷   )
6 idn3 43458 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑥𝐴   )
7 simpl 483 . . . . . . . . . . . 12 ((𝐴𝐵𝐶𝐷) → 𝐴𝐵)
83, 7e1a 43470 . . . . . . . . . . 11 (   (𝐴𝐵𝐶𝐷)   ▶   𝐴𝐵   )
9 idn2 43456 . . . . . . . . . . 11 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐵𝑦𝐷 𝜑   )
10 ssralv 4050 . . . . . . . . . . 11 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
118, 9, 10e12 43567 . . . . . . . . . 10 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐴𝑦𝐷 𝜑   )
12 df-ral 3062 . . . . . . . . . . 11 (∀𝑥𝐴𝑦𝐷 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
1312biimpi 215 . . . . . . . . . 10 (∀𝑥𝐴𝑦𝐷 𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
1411, 13e2 43474 . . . . . . . . 9 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑)   )
15 sp 2176 . . . . . . . . 9 (∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑) → (𝑥𝐴 → ∀𝑦𝐷 𝜑))
1614, 15e2 43474 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐷 𝜑)   )
17 pm2.27 42 . . . . . . . 8 (𝑥𝐴 → ((𝑥𝐴 → ∀𝑦𝐷 𝜑) → ∀𝑦𝐷 𝜑))
186, 16, 17e32 43601 . . . . . . 7 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑦𝐷 𝜑   )
19 ssralv 4050 . . . . . . 7 (𝐶𝐷 → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
205, 18, 19e13 43591 . . . . . 6 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑦𝐶 𝜑   )
2120in3 43452 . . . . 5 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐶 𝜑)   )
221, 2, 21gen21nv 43463 . . . 4 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑)   )
23 df-ral 3062 . . . . 5 (∀𝑥𝐴𝑦𝐶 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑))
2423biimpri 227 . . . 4 (∀𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑) → ∀𝑥𝐴𝑦𝐶 𝜑)
2522, 24e2 43474 . . 3 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐴𝑦𝐶 𝜑   )
2625in2 43448 . 2 (   (𝐴𝐵𝐶𝐷)   ▶   (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑)   )
2726in1 43414 1 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wal 1539  wcel 2106  wral 3061  wss 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-v 3476  df-in 3955  df-ss 3965  df-vd1 43413  df-vd2 43421  df-vd3 43433
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator