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	⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ( ∃ 𝑦 𝜑 → ∀ 𝑥 ∃ 𝑦 𝜑 ) )