Metamath Proof Explorer

Theorem hbexgVD

Description: Virtual deduction proof of hbexg . 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 is hbexgVD without virtual deductions and was automatically derived from hbexgVD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

1:: |- (. A. x A. y ( ph -> A. x ph ) ->. A. x A. y ( ph -> A. x ph ) ).
2:1: |- (. A. x A. y ( ph -> A. x ph ) ->. A. y A. x ( ph -> A. x ph ) ).
3:2: |- (. A. x A. y ( ph -> A. x ph ) ->. A. x ( ph -> A. x ph ) ).
4:3: |- (. A. x A. y ( ph -> A. x ph ) ->. A. x ( -. ph -> A. x -. ph ) ).
5:: |- ( A. x A. y ( ph -> A. x ph ) <-> A. y A. x ( ph -> A. x ph ) )
6:: |- ( A. y A. x ( ph -> A. x ph ) -> A. y A. y A. x ( ph -> A. x ph ) )
7:5: |- ( A. y A. x A. y ( ph -> A. x ph ) <-> A. y A. y A. x ( ph -> A. x ph ) )
8:5,6,7: |- ( A. x A. y ( ph -> A. x ph ) -> A. y A. x A. y ( ph -> A. x ph ) )
9:8,4: |- (. A. x A. y ( ph -> A. x ph ) ->. A. y A. x ( -. ph -> A. x -. ph ) ).
10:9: |- (. A. x A. y ( ph -> A. x ph ) ->. A. x A. y ( -. ph -> A. x -. ph ) ).
11:10: |- (. A. x A. y ( ph -> A. x ph ) ->. A. y ( -. ph -> A. x -. ph ) ).
12:11: |- (. A. x A. y ( ph -> A. x ph ) ->. A. y ( A. y -. ph -> A. x A. y -. ph ) ).
13:12: |- (. A. x A. y ( ph -> A. x ph ) ->. ( A. y -. ph -> A. x A. y -. ph ) ).
14:: |- ( A. x A. y ( ph -> A. x ph ) -> A. x A. x A. y ( ph -> A. x ph ) )
15:13,14: |- (. A. x A. y ( ph -> A. x ph ) ->. A. x ( A. y -. ph -> A. x A. y -. ph ) ).
16:15: |- (. A. x A. y ( ph -> A. x ph ) ->. A. x ( -. A. y -. ph -> A. x -. A. y -. ph ) ).
17:16: |- (. A. x A. y ( ph -> A. x ph ) ->. ( -. A. y -. ph -> A. x -. A. y -. ph ) ).
18:: |- ( E. y ph <-> -. A. y -. ph )
19:17,18: |- (. A. x A. y ( ph -> A. x ph ) ->. ( E. y ph -> A. x -. A. y -. ph ) ).
20:18: |- ( A. x E. y ph <-> A. x -. A. y -. ph )
21:19,20: |- (. A. x A. y ( ph -> A. x ph ) ->. ( E. y ph -> A. x E. y ph ) ).
22:8,21: |- (. A. x A. y ( ph -> A. x ph ) ->. A. y ( E. y ph -> A. x E. y ph ) ).
23:14,22: |- (. A. x A. y ( ph -> A. x ph ) ->. A. x A. y ( E. y ph -> A. x E. y ph ) ).
qed:23: |- (. A. x A. y ( ph -> A. x ph ) ->. A. x A. y ( E. y ph -> A. x E. y ph ) ).

Ref Expression
Assertion hbexgVD ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )

Proof

Step Hyp Ref Expression
1 hba1 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) )
2 hba1 ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑦 ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) )
3 alcom ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) )
4 3 albii ⊢ ( ∀ 𝑦 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) )
5 2 3 4 3imtr4i ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑦 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) )
6 idn1 ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    )
7 ax-11 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) )
8 6 7 e1a ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 )    )
9 sp ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) )
10 8 9 e1a ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 )    )
11 hbntal ⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
12 10 11 e1a ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑥 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 )    )
13 5 12 gen11nv ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑦 ∀ 𝑥 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 )    )
14 ax-11 ⊢ ( ∀ 𝑦 ∀ 𝑥 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
15 13 14 e1a ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑥 ∀ 𝑦 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 )    )
16 sp ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) → ∀ 𝑦 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
17 15 16 e1a ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑦 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 )    )
18 hbalg ⊢ ( ∀ 𝑦 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) → ∀ 𝑦 ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) )
19 17 18 e1a ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑦 ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 )    )
20 sp ⊢ ( ∀ 𝑦 ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) → ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) )
21 19 20 e1a ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 )    )
22 1 21 gen11nv ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑥 ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 )    )
23 hbntal ⊢ ( ∀ 𝑥 ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) → ∀ 𝑥 ( ¬ ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) )
24 22 23 e1a ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑥 ( ¬ ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 )    )
25 sp ⊢ ( ∀ 𝑥 ( ¬ ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) → ( ¬ ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) )
26 24 25 e1a ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ( ¬ ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 )    )
27 df-ex ⊢ ( ∃ 𝑦 𝜑 ↔ ¬ ∀ 𝑦 ¬ 𝜑 )
28 imbi1 ⊢ ( ( ∃ 𝑦 𝜑 ↔ ¬ ∀ 𝑦 ¬ 𝜑 ) → ( ( ∃ 𝑦 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) ↔ ( ¬ ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) ) )
29 28 biimprcd ⊢ ( ( ¬ ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) → ( ( ∃ 𝑦 𝜑 ↔ ¬ ∀ 𝑦 ¬ 𝜑 ) → ( ∃ 𝑦 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) ) )
30 26 27 29 e10 ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ( ∃ 𝑦 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 )    )
31 27 albii ⊢ ( ∀ 𝑥 ∃ 𝑦 𝜑 ↔ ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 )
32 imbi2 ⊢ ( ( ∀ 𝑥 ∃ 𝑦 𝜑 ↔ ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) → ( ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) ↔ ( ∃ 𝑦 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) ) )
33 32 biimprcd ⊢ ( ( ∃ 𝑦 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) → ( ( ∀ 𝑥 ∃ 𝑦 𝜑 ↔ ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) → ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) ) )
34 30 31 33 e10 ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 )    )
35 5 34 gen11nv ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑦 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 )    )
36 1 35 gen11nv ⊢ (    ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 )    ▶    ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 )    )
37 36 in1 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )