Theorem ax12indn

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Negation case. (Contributed by NM, 21-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ax12indn.1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
Assertion	ax12indn	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ¬ 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax12indn.1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
2		19.8a	⊢ ( ( 𝑥 = 𝑦 ∧ ¬ 𝜑 ) → ∃ 𝑥 ( 𝑥 = 𝑦 ∧ ¬ 𝜑 ) )
3		exanali	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ ¬ 𝜑 ) ↔ ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
4		hbn1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 )
5		hbn1	⊢ ( ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
6		con3	⊢ ( ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → ( ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ¬ 𝜑 ) )
7	1 6	syl6	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ¬ 𝜑 ) ) )
8	7	com23	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) )
9	4 5 8	alrimdh	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) )
10	3 9	syl5bi	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) )
11	2 10	syl5	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑥 = 𝑦 ∧ ¬ 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) )
12	11	expd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( ¬ 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) ) )