Theorem hbexgVD 46077

Description: Virtual deduction proof of hbexg 45728. 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 45728 is hbexgVD 46077 without virtual deductions and was automatically derived from hbexgVD 46077. (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

Step	Hyp	Ref	Expression
1		hba1 2330	. . 3 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
2		hba1 2330	. . . . 5 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
3		alcom 2199	. . . . 5 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
4	3	albii 1852	. . . . 5 ⊢ (∀𝑦∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
5	2, 3, 4	3imtr4i 295	. . . 4 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
6		idn1 45746	. . . . . . . . . . . . . . . . 17 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   )
7		ax-11 2197	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
8	6, 7	e1a 45799	. . . . . . . . . . . . . . . 16 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑)   )
9		sp 2223	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(𝜑 → ∀𝑥𝜑))
10	8, 9	e1a 45799	. . . . . . . . . . . . . . 15 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(𝜑 → ∀𝑥𝜑)   )
11		hbntal 45725	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
12	10, 11	e1a 45799	. . . . . . . . . . . . . 14 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
13	5, 12	gen11nv 45789	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
14		ax-11 2197	. . . . . . . . . . . . 13 ⊢ (∀𝑦∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
15	13, 14	e1a 45799	. . . . . . . . . . . 12 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
16		sp 2223	. . . . . . . . . . . 12 ⊢ (∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
17	15, 16	e1a 45799	. . . . . . . . . . 11 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
18		hbalg 45727	. . . . . . . . . . 11 ⊢ (∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑))
19	17, 18	e1a 45799	. . . . . . . . . 10 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
20		sp 2223	. . . . . . . . . 10 ⊢ (∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑) → (∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑))
21	19, 20	e1a 45799	. . . . . . . . 9 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
22	1, 21	gen11nv 45789	. . . . . . . 8 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
23		hbntal 45725	. . . . . . . 8 ⊢ (∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑) → ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
24	22, 23	e1a 45799	. . . . . . 7 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
25		sp 2223	. . . . . . 7 ⊢ (∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
26	24, 25	e1a 45799	. . . . . 6 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
27		df-ex 1813	. . . . . 6 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
28		imbi1 350	. . . . . . 7 ⊢ ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) ↔ (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
29	28	biimprcd 253	. . . . . 6 ⊢ ((¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
30	26, 27, 29	e10 45866	. . . . 5 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
31	27	albii 1852	. . . . 5 ⊢ (∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)
32		imbi2 351	. . . . . 6 ⊢ ((∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) ↔ (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
33	32	biimprcd 253	. . . . 5 ⊢ ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)))
34	30, 31, 33	e10 45866	. . . 4 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
35	5, 34	gen11nv 45789	. . 3 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
36	1, 35	gen11nv 45789	. 2 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
37	36	in1 45743	1 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-10 2180  ax-11 2197  ax-12 2216

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817  df-vd1 45742

This theorem is used by: (None)