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

Theorem hbexgVD 41605
Description: Virtual deduction proof of hbexg 41255. 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. hbexg 41255 is hbexgVD 41605 without virtual deductions and was automatically derived from hbexgVD 41605. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1:: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥 𝑦(𝜑 → ∀𝑥𝜑)   )
2:1: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦 𝑥(𝜑 → ∀𝑥𝜑)   )
3:2: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥 (𝜑 → ∀𝑥𝜑)   )
4:3: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥 𝜑 → ∀𝑥¬ 𝜑)   )
5:: (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦 𝑥(𝜑 → ∀𝑥𝜑))
6:: (∀𝑦𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑦 𝑦𝑥(𝜑 → ∀𝑥𝜑))
7:5: (∀𝑦𝑥𝑦(𝜑 → ∀𝑥𝜑) ↔ 𝑦𝑦𝑥(𝜑 → ∀𝑥𝜑))
8:5,6,7: (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦 𝑥𝑦(𝜑 → ∀𝑥𝜑))
9:8,4: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦 𝑥𝜑 → ∀𝑥¬ 𝜑)   )
10:9: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥 𝑦𝜑 → ∀𝑥¬ 𝜑)   )
11:10: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦 𝜑 → ∀𝑥¬ 𝜑)   )
12:11: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦 (∀𝑦¬ 𝜑 → ∀𝑥𝑦¬ 𝜑)   )
13:12: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀ 𝑦¬ 𝜑 → ∀𝑥𝑦¬ 𝜑)   )
14:: (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥 𝑥𝑦(𝜑 → ∀𝑥𝜑))
15:13,14: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥 (∀𝑦¬ 𝜑 → ∀𝑥𝑦¬ 𝜑)   )
16:15: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥 (¬ ∀𝑦¬ 𝜑 → ∀𝑥¬ ∀𝑦¬ 𝜑)   )
17:16: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶    𝑦¬ 𝜑 → ∀𝑥¬ ∀𝑦¬ 𝜑)   )
18:: (∃𝑦𝜑 ↔ ¬ ∀𝑦¬ 𝜑)
19:17,18: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃ 𝑦𝜑 → ∀𝑥¬ ∀𝑦¬ 𝜑)   )
20:18: (∀𝑥𝑦𝜑 ↔ ∀𝑥¬ ∀𝑦¬ 𝜑)
21:19,20: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃ 𝑦𝜑 → ∀𝑥𝑦𝜑)   )
22:8,21: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦 (∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
23:14,22: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥 𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
qed:23: (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥 𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
Assertion
Ref Expression
hbexgVD (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑))

Proof of Theorem hbexgVD
StepHypRef Expression
1 hba1 2299 . . 3 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑥𝑦(𝜑 → ∀𝑥𝜑))
2 hba1 2299 . . . . 5 (∀𝑦𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑦𝑦𝑥(𝜑 → ∀𝑥𝜑))
3 alcom 2161 . . . . 5 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦𝑥(𝜑 → ∀𝑥𝜑))
43albii 1821 . . . . 5 (∀𝑦𝑥𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦𝑦𝑥(𝜑 → ∀𝑥𝜑))
52, 3, 43imtr4i 295 . . . 4 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦𝑥𝑦(𝜑 → ∀𝑥𝜑))
6 idn1 41273 . . . . . . . . . . . . . . . . 17 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝑦(𝜑 → ∀𝑥𝜑)   )
7 ax-11 2159 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦𝑥(𝜑 → ∀𝑥𝜑))
86, 7e1a 41326 . . . . . . . . . . . . . . . 16 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦𝑥(𝜑 → ∀𝑥𝜑)   )
9 sp 2181 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(𝜑 → ∀𝑥𝜑))
108, 9e1a 41326 . . . . . . . . . . . . . . 15 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥(𝜑 → ∀𝑥𝜑)   )
11 hbntal 41252 . . . . . . . . . . . . . . 15 (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝜑 → ∀𝑥 ¬ 𝜑))
1210, 11e1a 41326 . . . . . . . . . . . . . 14 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝜑 → ∀𝑥 ¬ 𝜑)   )
135, 12gen11nv 41316 . . . . . . . . . . . . 13 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦𝑥𝜑 → ∀𝑥 ¬ 𝜑)   )
14 ax-11 2159 . . . . . . . . . . . . 13 (∀𝑦𝑥𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥𝑦𝜑 → ∀𝑥 ¬ 𝜑))
1513, 14e1a 41326 . . . . . . . . . . . 12 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝑦𝜑 → ∀𝑥 ¬ 𝜑)   )
16 sp 2181 . . . . . . . . . . . 12 (∀𝑥𝑦𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦𝜑 → ∀𝑥 ¬ 𝜑))
1715, 16e1a 41326 . . . . . . . . . . 11 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦𝜑 → ∀𝑥 ¬ 𝜑)   )
18 hbalg 41254 . . . . . . . . . . 11 (∀𝑦𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑))
1917, 18e1a 41326 . . . . . . . . . 10 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑)   )
20 sp 2181 . . . . . . . . . 10 (∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑) → (∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑))
2119, 20e1a 41326 . . . . . . . . 9 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑)   )
221, 21gen11nv 41316 . . . . . . . 8 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑)   )
23 hbntal 41252 . . . . . . . 8 (∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑) → ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
2422, 23e1a 41326 . . . . . . 7 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
25 sp 2181 . . . . . . 7 (∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
2624, 25e1a 41326 . . . . . 6 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
27 df-ex 1782 . . . . . 6 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
28 imbi1 351 . . . . . . 7 ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) ↔ (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
2928biimprcd 253 . . . . . 6 ((¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
3026, 27, 29e10 41393 . . . . 5 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
3127albii 1821 . . . . 5 (∀𝑥𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)
32 imbi2 352 . . . . . 6 ((∀𝑥𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥𝑦𝜑) ↔ (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
3332biimprcd 253 . . . . 5 ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∀𝑥𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥𝑦𝜑)))
3430, 31, 33e10 41393 . . . 4 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
355, 34gen11nv 41316 . . 3 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
361, 35gen11nv 41316 . 2 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
3736in1 41270 1 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wal 1536  wex 1781
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 1911  ax-6 1970  ax-7 2015  ax-10 2143  ax-11 2159  ax-12 2176
This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782  df-nf 1786  df-vd1 41269
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator