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 39619
Description: Quantification restricted to a subclass for two quantifiers. ssralv 3807 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 39257 is ssralv2VD 39619 without virtual deductions and was automatically derived from ssralv2VD 39619.
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 1988 . . . . 5 ((𝐴𝐵𝐶𝐷) → ∀𝑥(𝐴𝐵𝐶𝐷))
2 hbra1 3080 . . . . 5 (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝑥𝐵𝑦𝐷 𝜑)
3 idn1 39310 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ▶   (𝐴𝐵𝐶𝐷)   )
4 simpr 479 . . . . . . . 8 ((𝐴𝐵𝐶𝐷) → 𝐶𝐷)
53, 4e1a 39372 . . . . . . 7 (   (𝐴𝐵𝐶𝐷)   ▶   𝐶𝐷   )
6 idn3 39360 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑥𝐴   )
7 simpl 474 . . . . . . . . . . . 12 ((𝐴𝐵𝐶𝐷) → 𝐴𝐵)
83, 7e1a 39372 . . . . . . . . . . 11 (   (𝐴𝐵𝐶𝐷)   ▶   𝐴𝐵   )
9 idn2 39358 . . . . . . . . . . 11 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐵𝑦𝐷 𝜑   )
10 ssralv 3807 . . . . . . . . . . 11 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
118, 9, 10e12 39471 . . . . . . . . . 10 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐴𝑦𝐷 𝜑   )
12 df-ral 3055 . . . . . . . . . . 11 (∀𝑥𝐴𝑦𝐷 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
1312biimpi 206 . . . . . . . . . 10 (∀𝑥𝐴𝑦𝐷 𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
1411, 13e2 39376 . . . . . . . . 9 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑)   )
15 sp 2200 . . . . . . . . 9 (∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑) → (𝑥𝐴 → ∀𝑦𝐷 𝜑))
1614, 15e2 39376 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐷 𝜑)   )
17 pm2.27 42 . . . . . . . 8 (𝑥𝐴 → ((𝑥𝐴 → ∀𝑦𝐷 𝜑) → ∀𝑦𝐷 𝜑))
186, 16, 17e32 39505 . . . . . . 7 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑦𝐷 𝜑   )
19 ssralv 3807 . . . . . . 7 (𝐶𝐷 → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
205, 18, 19e13 39495 . . . . . 6 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑦𝐶 𝜑   )
2120in3 39354 . . . . 5 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐶 𝜑)   )
221, 2, 21gen21nv 39365 . . . 4 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑)   )
23 df-ral 3055 . . . . 5 (∀𝑥𝐴𝑦𝐶 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑))
2423biimpri 218 . . . 4 (∀𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑) → ∀𝑥𝐴𝑦𝐶 𝜑)
2522, 24e2 39376 . . 3 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐴𝑦𝐶 𝜑   )
2625in2 39350 . 2 (   (𝐴𝐵𝐶𝐷)   ▶   (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑)   )
2726in1 39307 1 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1630  wcel 2139  wral 3050  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-ral 3055  df-in 3722  df-ss 3729  df-vd1 39306  df-vd2 39314  df-vd3 39326
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator