Theorem hbexgVD 45486

Description: Virtual deduction proof of hbexg 45137. 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 45137 is hbexgVD 45486 without virtual deductions and was automatically derived from hbexgVD 45486. (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 2329	. . 3 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
2		hba1 2329	. . . . 5 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
3		alcom 2195	. . . . 5 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
4	3	albii 1841	. . . . 5 ⊢ (∀𝑦∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
5	2, 3, 4	3imtr4i 294	. . . 4 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
6		idn1 45155	. . . . . . . . . . . . . . . . 17 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   )
7		ax-11 2193	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
8	6, 7	e1a 45208	. . . . . . . . . . . . . . . 16 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑)   )
9		sp 2220	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(𝜑 → ∀𝑥𝜑))
10	8, 9	e1a 45208	. . . . . . . . . . . . . . 15 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(𝜑 → ∀𝑥𝜑)   )
11		hbntal 45134	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
12	10, 11	e1a 45208	. . . . . . . . . . . . . 14 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
13	5, 12	gen11nv 45198	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
14		ax-11 2193	. . . . . . . . . . . . 13 ⊢ (∀𝑦∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
15	13, 14	e1a 45208	. . . . . . . . . . . 12 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
16		sp 2220	. . . . . . . . . . . 12 ⊢ (∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
17	15, 16	e1a 45208	. . . . . . . . . . 11 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
18		hbalg 45136	. . . . . . . . . . 11 ⊢ (∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑))
19	17, 18	e1a 45208	. . . . . . . . . 10 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
20		sp 2220	. . . . . . . . . 10 ⊢ (∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑) → (∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑))
21	19, 20	e1a 45208	. . . . . . . . 9 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
22	1, 21	gen11nv 45198	. . . . . . . 8 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
23		hbntal 45134	. . . . . . . 8 ⊢ (∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑) → ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
24	22, 23	e1a 45208	. . . . . . 7 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
25		sp 2220	. . . . . . 7 ⊢ (∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
26	24, 25	e1a 45208	. . . . . 6 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
27		df-ex 1802	. . . . . 6 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
28		imbi1 349	. . . . . . 7 ⊢ ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) ↔ (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
29	28	biimprcd 252	. . . . . 6 ⊢ ((¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
30	26, 27, 29	e10 45275	. . . . 5 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
31	27	albii 1841	. . . . 5 ⊢ (∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)
32		imbi2 350	. . . . . 6 ⊢ ((∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) ↔ (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
33	32	biimprcd 252	. . . . 5 ⊢ ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)))
34	30, 31, 33	e10 45275	. . . 4 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
35	5, 34	gen11nv 45198	. . 3 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
36	1, 35	gen11nv 45198	. 2 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
37	36	in1 45152	1 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208  ∀wal 1560  ∃wex 1801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-10 2177  ax-11 2193  ax-12 2214

This theorem depends on definitions:  df-bi 209  df-or 859  df-ex 1802  df-nf 1806  df-vd1 45151

This theorem is referenced by: (None)