Theorem hbexgVD 45362

Description: Virtual deduction proof of hbexg 45013. 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 45013 is hbexgVD 45362 without virtual deductions and was automatically derived from hbexgVD 45362. (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 2306	. . 3 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
2		hba1 2306	. . . . 5 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
3		alcom 2172	. . . . 5 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
4	3	albii 1827	. . . . 5 ⊢ (∀𝑦∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
5	2, 3, 4	3imtr4i 294	. . . 4 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
6		idn1 45031	. . . . . . . . . . . . . . . . 17 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   )
7		ax-11 2170	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
8	6, 7	e1a 45084	. . . . . . . . . . . . . . . 16 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑)   )
9		sp 2197	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(𝜑 → ∀𝑥𝜑))
10	8, 9	e1a 45084	. . . . . . . . . . . . . . 15 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(𝜑 → ∀𝑥𝜑)   )
11		hbntal 45010	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
12	10, 11	e1a 45084	. . . . . . . . . . . . . 14 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
13	5, 12	gen11nv 45074	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
14		ax-11 2170	. . . . . . . . . . . . 13 ⊢ (∀𝑦∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
15	13, 14	e1a 45084	. . . . . . . . . . . 12 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
16		sp 2197	. . . . . . . . . . . 12 ⊢ (∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
17	15, 16	e1a 45084	. . . . . . . . . . 11 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
18		hbalg 45012	. . . . . . . . . . 11 ⊢ (∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑))
19	17, 18	e1a 45084	. . . . . . . . . 10 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
20		sp 2197	. . . . . . . . . 10 ⊢ (∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑) → (∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑))
21	19, 20	e1a 45084	. . . . . . . . 9 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
22	1, 21	gen11nv 45074	. . . . . . . 8 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
23		hbntal 45010	. . . . . . . 8 ⊢ (∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑) → ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
24	22, 23	e1a 45084	. . . . . . 7 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
25		sp 2197	. . . . . . 7 ⊢ (∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
26	24, 25	e1a 45084	. . . . . 6 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
27		df-ex 1788	. . . . . 6 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
28		imbi1 349	. . . . . . 7 ⊢ ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) ↔ (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
29	28	biimprcd 252	. . . . . 6 ⊢ ((¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
30	26, 27, 29	e10 45151	. . . . 5 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
31	27	albii 1827	. . . . 5 ⊢ (∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)
32		imbi2 350	. . . . . 6 ⊢ ((∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) ↔ (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
33	32	biimprcd 252	. . . . 5 ⊢ ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)))
34	30, 31, 33	e10 45151	. . . 4 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
35	5, 34	gen11nv 45074	. . 3 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
36	1, 35	gen11nv 45074	. 2 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
37	36	in1 45028	1 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-10 2154  ax-11 2170  ax-12 2191

This theorem depends on definitions:  df-bi 209  df-or 855  df-ex 1788  df-nf 1792  df-vd1 45027

This theorem is referenced by: (None)