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 37963
Description: Virtual deduction proof of hbexg 37592. 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 37592 is hbexgVD 37963 without virtual deductions and was automatically derived from hbexgVD 37963. (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 2134 . . 3 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑥𝑦(𝜑 → ∀𝑥𝜑))
2 hba1 2134 . . . . 5 (∀𝑦𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑦𝑦𝑥(𝜑 → ∀𝑥𝜑))
3 alcom 2022 . . . . 5 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦𝑥(𝜑 → ∀𝑥𝜑))
43albii 1735 . . . . 5 (∀𝑦𝑥𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦𝑦𝑥(𝜑 → ∀𝑥𝜑))
52, 3, 43imtr4i 279 . . . 4 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦𝑥𝑦(𝜑 → ∀𝑥𝜑))
6 idn1 37610 . . . . . . . . . . . . . . . . 17 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝑦(𝜑 → ∀𝑥𝜑)   )
7 ax-11 2019 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦𝑥(𝜑 → ∀𝑥𝜑))
86, 7e1a 37672 . . . . . . . . . . . . . . . 16 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦𝑥(𝜑 → ∀𝑥𝜑)   )
9 sp 2038 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(𝜑 → ∀𝑥𝜑))
108, 9e1a 37672 . . . . . . . . . . . . . . 15 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥(𝜑 → ∀𝑥𝜑)   )
11 hbntal 37589 . . . . . . . . . . . . . . 15 (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝜑 → ∀𝑥 ¬ 𝜑))
1210, 11e1a 37672 . . . . . . . . . . . . . 14 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝜑 → ∀𝑥 ¬ 𝜑)   )
135, 12gen11nv 37662 . . . . . . . . . . . . 13 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦𝑥𝜑 → ∀𝑥 ¬ 𝜑)   )
14 ax-11 2019 . . . . . . . . . . . . 13 (∀𝑦𝑥𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥𝑦𝜑 → ∀𝑥 ¬ 𝜑))
1513, 14e1a 37672 . . . . . . . . . . . 12 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝑦𝜑 → ∀𝑥 ¬ 𝜑)   )
16 sp 2038 . . . . . . . . . . . 12 (∀𝑥𝑦𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦𝜑 → ∀𝑥 ¬ 𝜑))
1715, 16e1a 37672 . . . . . . . . . . 11 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦𝜑 → ∀𝑥 ¬ 𝜑)   )
18 hbalg 37591 . . . . . . . . . . 11 (∀𝑦𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑))
1917, 18e1a 37672 . . . . . . . . . 10 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑)   )
20 sp 2038 . . . . . . . . . 10 (∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑) → (∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑))
2119, 20e1a 37672 . . . . . . . . 9 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑)   )
221, 21gen11nv 37662 . . . . . . . 8 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑)   )
23 hbntal 37589 . . . . . . . 8 (∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑) → ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
2422, 23e1a 37672 . . . . . . 7 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
25 sp 2038 . . . . . . 7 (∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
2624, 25e1a 37672 . . . . . 6 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
27 df-ex 1695 . . . . . 6 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
28 imbi1 335 . . . . . . 7 ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) ↔ (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
2928biimprcd 238 . . . . . 6 ((¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
3026, 27, 29e10 37739 . . . . 5 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
3127albii 1735 . . . . 5 (∀𝑥𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)
32 imbi2 336 . . . . . 6 ((∀𝑥𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥𝑦𝜑) ↔ (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
3332biimprcd 238 . . . . 5 ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∀𝑥𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥𝑦𝜑)))
3430, 31, 33e10 37739 . . . 4 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
355, 34gen11nv 37662 . . 3 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
361, 35gen11nv 37662 . 2 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
3736in1 37607 1 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031
This theorem depends on definitions:  df-bi 195  df-or 383  df-ex 1695  df-nf 1700  df-vd1 37606
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator