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

Theorem ssralv2VD 41065
Description: Quantification restricted to a subclass for two quantifiers. ssralv 4037 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 40730 is ssralv2VD 41065 without virtual deductions and was automatically derived from ssralv2VD 41065.
 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 1904 . . . . 5 ((𝐴𝐵𝐶𝐷) → ∀𝑥(𝐴𝐵𝐶𝐷))
2 hbra1 3225 . . . . 5 (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝑥𝐵𝑦𝐷 𝜑)
3 idn1 40773 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ▶   (𝐴𝐵𝐶𝐷)   )
4 simpr 485 . . . . . . . 8 ((𝐴𝐵𝐶𝐷) → 𝐶𝐷)
53, 4e1a 40826 . . . . . . 7 (   (𝐴𝐵𝐶𝐷)   ▶   𝐶𝐷   )
6 idn3 40814 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑥𝐴   )
7 simpl 483 . . . . . . . . . . . 12 ((𝐴𝐵𝐶𝐷) → 𝐴𝐵)
83, 7e1a 40826 . . . . . . . . . . 11 (   (𝐴𝐵𝐶𝐷)   ▶   𝐴𝐵   )
9 idn2 40812 . . . . . . . . . . 11 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐵𝑦𝐷 𝜑   )
10 ssralv 4037 . . . . . . . . . . 11 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐷 𝜑))
118, 9, 10e12 40923 . . . . . . . . . 10 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐴𝑦𝐷 𝜑   )
12 df-ral 3148 . . . . . . . . . . 11 (∀𝑥𝐴𝑦𝐷 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
1312biimpi 217 . . . . . . . . . 10 (∀𝑥𝐴𝑦𝐷 𝜑 → ∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑))
1411, 13e2 40830 . . . . . . . . 9 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑)   )
15 sp 2174 . . . . . . . . 9 (∀𝑥(𝑥𝐴 → ∀𝑦𝐷 𝜑) → (𝑥𝐴 → ∀𝑦𝐷 𝜑))
1614, 15e2 40830 . . . . . . . 8 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐷 𝜑)   )
17 pm2.27 42 . . . . . . . 8 (𝑥𝐴 → ((𝑥𝐴 → ∀𝑦𝐷 𝜑) → ∀𝑦𝐷 𝜑))
186, 16, 17e32 40957 . . . . . . 7 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑦𝐷 𝜑   )
19 ssralv 4037 . . . . . . 7 (𝐶𝐷 → (∀𝑦𝐷 𝜑 → ∀𝑦𝐶 𝜑))
205, 18, 19e13 40947 . . . . . 6 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ,   𝑥𝐴   ▶   𝑦𝐶 𝜑   )
2120in3 40808 . . . . 5 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   (𝑥𝐴 → ∀𝑦𝐶 𝜑)   )
221, 2, 21gen21nv 40819 . . . 4 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑)   )
23 df-ral 3148 . . . . 5 (∀𝑥𝐴𝑦𝐶 𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑))
2423biimpri 229 . . . 4 (∀𝑥(𝑥𝐴 → ∀𝑦𝐶 𝜑) → ∀𝑥𝐴𝑦𝐶 𝜑)
2522, 24e2 40830 . . 3 (   (𝐴𝐵𝐶𝐷)   ,   𝑥𝐵𝑦𝐷 𝜑   ▶   𝑥𝐴𝑦𝐶 𝜑   )
2625in2 40804 . 2 (   (𝐴𝐵𝐶𝐷)   ▶   (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑)   )
2726in1 40770 1 ((𝐴𝐵𝐶𝐷) → (∀𝑥𝐵𝑦𝐷 𝜑 → ∀𝑥𝐴𝑦𝐶 𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1528   ∈ wcel 2107  ∀wral 3143   ⊆ wss 3940 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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-ral 3148  df-in 3947  df-ss 3956  df-vd1 40769  df-vd2 40777  df-vd3 40789 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator