Theorem axc5c4c711

Description: Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen as the inference rule. This proof extends the idea of axc5c711 and related theorems. (Contributed by Andrew Salmon, 14-Jul-2011)

	Ref	Expression
Assertion	axc5c4c711	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) ) ) → ( ∀ 𝑦 𝜑 → ∀ 𝑦 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		axc4	⊢ ( ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) → ( ∀ 𝑦 𝜑 → ∀ 𝑦 𝜓 ) )
2		hbn1	⊢ ( ¬ ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) → ∀ 𝑦 ¬ ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) )
3		axc7	⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) → ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) )
4	3	con1i	⊢ ( ¬ ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) → ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) )
5	2 4	alrimih	⊢ ( ¬ ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) → ∀ 𝑦 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) )
6		ax-11	⊢ ( ∀ 𝑦 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) → ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) )
7	5 6	syl	⊢ ( ¬ ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) → ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) )
8	1 7	nsyl4	⊢ ( ¬ ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) → ( ∀ 𝑦 𝜑 → ∀ 𝑦 𝜓 ) )
9		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → ∀ 𝑦 𝜓 ) )
10	9	spsd	⊢ ( ¬ 𝜑 → ( ∀ 𝑦 𝜑 → ∀ 𝑦 𝜓 ) )
11	10 1	ja	⊢ ( ( 𝜑 → ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) ) → ( ∀ 𝑦 𝜑 → ∀ 𝑦 𝜓 ) )
12	8 11	ja	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ¬ ∀ 𝑥 ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑦 ( ∀ 𝑦 𝜑 → 𝜓 ) ) ) → ( ∀ 𝑦 𝜑 → ∀ 𝑦 𝜓 ) )