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 43930
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 43595 is ssralv2VD 43930 without virtual deductions and was automatically derived from ssralv2VD 43930.
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 1912 . . . . 5 ((𝐴𝐵𝐶𝐷) → ∀𝑥(𝐴𝐵𝐶𝐷))
2 hbra1 3297 . . . . 5 (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝑥𝐵𝑦𝐷 𝜑)
3 idn1 43638 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ▶   (𝐴𝐵𝐶𝐷)   )
4 simpr 484 . . . . . . . 8 ((𝐴𝐵𝐶𝐷) → 𝐶𝐷)
53, 4e1a 43691 . . . . . . 7 (   (𝐴𝐵𝐶𝐷)   ▶   𝐶𝐷   )
6 idn3 43679 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑥𝐴   )
7 simpl 482 . . . . . . . . . . . 12 ((𝐴𝐵𝐶𝐷) → 𝐴𝐵)
83, 7e1a 43691 . . . . . . . . . . 11 (   (𝐴𝐵𝐶𝐷)   ▶   𝐴𝐵   )
9 idn2 43677 . . . . . . . . . . 11 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐵𝑦𝐷 𝜑   )
10 ssralv 4050 . . . . . . . . . . 11 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
118, 9, 10e12 43788 . . . . . . . . . 10 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐴𝑦𝐷 𝜑   )
12 df-ral 3061 . . . . . . . . . . 11 (∀𝑥𝐴𝑦𝐷 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
1312biimpi 215 . . . . . . . . . 10 (∀𝑥𝐴𝑦𝐷 𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
1411, 13e2 43695 . . . . . . . . 9 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑)   )
15 sp 2175 . . . . . . . . 9 (∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑) → (𝑥𝐴 → ∀𝑦𝐷 𝜑))
1614, 15e2 43695 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐷 𝜑)   )
17 pm2.27 42 . . . . . . . 8 (𝑥𝐴 → ((𝑥𝐴 → ∀𝑦𝐷 𝜑) → ∀𝑦𝐷 𝜑))
186, 16, 17e32 43822 . . . . . . 7 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑦𝐷 𝜑   )
19 ssralv 4050 . . . . . . 7 (𝐶𝐷 → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
205, 18, 19e13 43812 . . . . . 6 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑦𝐶 𝜑   )
2120in3 43673 . . . . 5 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐶 𝜑)   )
221, 2, 21gen21nv 43684 . . . 4 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑)   )
23 df-ral 3061 . . . . 5 (∀𝑥𝐴𝑦𝐶 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑))
2423biimpri 227 . . . 4 (∀𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑) → ∀𝑥𝐴𝑦𝐶 𝜑)
2522, 24e2 43695 . . 3 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐴𝑦𝐶 𝜑   )
2625in2 43669 . 2 (   (𝐴𝐵𝐶𝐷)   ▶   (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑)   )
2726in1 43635 1 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1538  wcel 2105  wral 3060  wss 3948
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-12 2170  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-ex 1781  df-nf 1785  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-v 3475  df-in 3955  df-ss 3965  df-vd1 43634  df-vd2 43642  df-vd3 43654
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator