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 43969
Description: Virtual deduction proof of hbexg 43619. 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 43619 is hbexgVD 43969 without virtual deductions and was automatically derived from hbexgVD 43969. (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 2287 . . 3 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑥𝑦(𝜑 → ∀𝑥𝜑))
2 hba1 2287 . . . . 5 (∀𝑦𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑦𝑦𝑥(𝜑 → ∀𝑥𝜑))
3 alcom 2154 . . . . 5 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦𝑥(𝜑 → ∀𝑥𝜑))
43albii 1819 . . . . 5 (∀𝑦𝑥𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦𝑦𝑥(𝜑 → ∀𝑥𝜑))
52, 3, 43imtr4i 291 . . . 4 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦𝑥𝑦(𝜑 → ∀𝑥𝜑))
6 idn1 43637 . . . . . . . . . . . . . . . . 17 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝑦(𝜑 → ∀𝑥𝜑)   )
7 ax-11 2152 . . . . . . . . . . . . . . . . 17 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦𝑥(𝜑 → ∀𝑥𝜑))
86, 7e1a 43690 . . . . . . . . . . . . . . . 16 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦𝑥(𝜑 → ∀𝑥𝜑)   )
9 sp 2174 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(𝜑 → ∀𝑥𝜑))
108, 9e1a 43690 . . . . . . . . . . . . . . 15 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥(𝜑 → ∀𝑥𝜑)   )
11 hbntal 43616 . . . . . . . . . . . . . . 15 (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥𝜑 → ∀𝑥 ¬ 𝜑))
1210, 11e1a 43690 . . . . . . . . . . . . . 14 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝜑 → ∀𝑥 ¬ 𝜑)   )
135, 12gen11nv 43680 . . . . . . . . . . . . 13 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦𝑥𝜑 → ∀𝑥 ¬ 𝜑)   )
14 ax-11 2152 . . . . . . . . . . . . 13 (∀𝑦𝑥𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥𝑦𝜑 → ∀𝑥 ¬ 𝜑))
1513, 14e1a 43690 . . . . . . . . . . . 12 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝑦𝜑 → ∀𝑥 ¬ 𝜑)   )
16 sp 2174 . . . . . . . . . . . 12 (∀𝑥𝑦𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦𝜑 → ∀𝑥 ¬ 𝜑))
1715, 16e1a 43690 . . . . . . . . . . 11 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦𝜑 → ∀𝑥 ¬ 𝜑)   )
18 hbalg 43618 . . . . . . . . . . 11 (∀𝑦𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑))
1917, 18e1a 43690 . . . . . . . . . 10 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑)   )
20 sp 2174 . . . . . . . . . 10 (∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑) → (∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑))
2119, 20e1a 43690 . . . . . . . . 9 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑)   )
221, 21gen11nv 43680 . . . . . . . 8 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑)   )
23 hbntal 43616 . . . . . . . 8 (∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥𝑦 ¬ 𝜑) → ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
2422, 23e1a 43690 . . . . . . 7 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
25 sp 2174 . . . . . . 7 (∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
2624, 25e1a 43690 . . . . . 6 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
27 df-ex 1780 . . . . . 6 (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
28 imbi1 346 . . . . . . 7 ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) ↔ (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
2928biimprcd 249 . . . . . 6 ((¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
3026, 27, 29e10 43757 . . . . 5 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
3127albii 1819 . . . . 5 (∀𝑥𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)
32 imbi2 347 . . . . . 6 ((∀𝑥𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥𝑦𝜑) ↔ (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
3332biimprcd 249 . . . . 5 ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∀𝑥𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥𝑦𝜑)))
3430, 31, 33e10 43757 . . . 4 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
355, 34gen11nv 43680 . . 3 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
361, 35gen11nv 43680 . 2 (   𝑥𝑦(𝜑 → ∀𝑥𝜑)   ▶   𝑥𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑)   )
3736in1 43634 1 (∀𝑥𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥𝑦(∃𝑦𝜑 → ∀𝑥𝑦𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wal 1537  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-10 2135  ax-11 2152  ax-12 2169
This theorem depends on definitions:  df-bi 206  df-or 844  df-ex 1780  df-nf 1784  df-vd1 43633
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator