Theorem hbexgVD 39654

Description: Virtual deduction proof of hbexg 39288. 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 39288 is hbexgVD 39654 without virtual deductions and was automatically derived from hbexgVD 39654. (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 2205	. . . . 5 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
4	3	albii 1904	. . . . 5 ⊢ (∀𝑦∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) ↔ ∀𝑦∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
5	2, 3, 4	3imtr4i 283	. . . 4 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑))
6		idn1 39306	. . . . . . . . . . . . . . . . 17 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   )
7		ax-11 2202	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑))
8	6, 7	e1a 39368	. . . . . . . . . . . . . . . 16 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑)   )
9		sp 2219	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(𝜑 → ∀𝑥𝜑))
10	8, 9	e1a 39368	. . . . . . . . . . . . . . 15 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(𝜑 → ∀𝑥𝜑)   )
11		hbntal 39285	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
12	10, 11	e1a 39368	. . . . . . . . . . . . . 14 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
13	5, 12	gen11nv 39358	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
14		ax-11 2202	. . . . . . . . . . . . 13 ⊢ (∀𝑦∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
15	13, 14	e1a 39368	. . . . . . . . . . . 12 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
16		sp 2219	. . . . . . . . . . . 12 ⊢ (∀𝑥∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑))
17	15, 16	e1a 39368	. . . . . . . . . . 11 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑)   )
18		hbalg 39287	. . . . . . . . . . 11 ⊢ (∀𝑦(¬ 𝜑 → ∀𝑥 ¬ 𝜑) → ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑))
19	17, 18	e1a 39368	. . . . . . . . . 10 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
20		sp 2219	. . . . . . . . . 10 ⊢ (∀𝑦(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑) → (∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑))
21	19, 20	e1a 39368	. . . . . . . . 9 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
22	1, 21	gen11nv 39358	. . . . . . . 8 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑)   )
23		hbntal 39285	. . . . . . . 8 ⊢ (∀𝑥(∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦 ¬ 𝜑) → ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
24	22, 23	e1a 39368	. . . . . . 7 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
25		sp 2219	. . . . . . 7 ⊢ (∀𝑥(¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑))
26	24, 25	e1a 39368	. . . . . 6 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
27		df-ex 1860	. . . . . 6 ⊢ (∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑)
28		imbi1 338	. . . . . . 7 ⊢ ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) ↔ (¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
29	28	biimprcd 241	. . . . . 6 ⊢ ((¬ ∀𝑦 ¬ 𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 ↔ ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
30	26, 27, 29	e10 39435	. . . . 5 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)   )
31	27	albii 1904	. . . . 5 ⊢ (∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)
32		imbi2 339	. . . . . 6 ⊢ ((∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∃𝑦𝜑 → ∀𝑥∃𝑦𝜑) ↔ (∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑)))
33	32	biimprcd 241	. . . . 5 ⊢ ((∃𝑦𝜑 → ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → ((∀𝑥∃𝑦𝜑 ↔ ∀𝑥 ¬ ∀𝑦 ¬ 𝜑) → (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)))
34	30, 31, 33	e10 39435	. . . 4 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
35	5, 34	gen11nv 39358	. . 3 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
36	1, 35	gen11nv 39358	. 2 ⊢ (   ∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑)   ▶   ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)   )
37	36	in1 39303	1 ⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197  ∀wal 1635  ∃wex 1859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-10 2186  ax-11 2202  ax-12 2215

This theorem depends on definitions:  df-bi 198  df-or 866  df-ex 1860  df-nf 1864  df-vd1 39302

This theorem is referenced by: (None)