This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bj-hbext

Description: Closed form of hbex . (Contributed by BJ, 10-Oct-2019)

Ref Expression
Assertion bj-hbext ( ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )

Proof

Step Hyp Ref Expression
1 nfa2 ⊢ Ⅎ 𝑥 ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 )
2 hbnt ⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
3 2 alimi ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑦 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
4 bj-hbalt ⊢ ( ∀ 𝑦 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) → ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) )
5 3 4 syl ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) )
6 1 5 alrimi ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) )
7 hbnt ⊢ ( ∀ 𝑥 ( ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 ) → ( ¬ ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) )
8 6 7 syl ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ¬ ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ) )
9 df-ex ⊢ ( ∃ 𝑦 𝜑 ↔ ¬ ∀ 𝑦 ¬ 𝜑 )
10 9 bicomi ⊢ ( ¬ ∀ 𝑦 ¬ 𝜑 ↔ ∃ 𝑦 𝜑 )
11 10 albii ⊢ ( ∀ 𝑥 ¬ ∀ 𝑦 ¬ 𝜑 ↔ ∀ 𝑥 ∃ 𝑦 𝜑 )
12 8 10 11 3imtr3g ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )