axc15

Description: Derivation of set.mm's original ax-c15 from ax-c11n and the shorter ax-12 that has replaced it.

Normally, axc15 should be used rather than ax-c15 , except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Feb-2007) (Proof shortened by Wolf Lammen, 26-Mar-2023) (New usage is discouraged.)

		Ref	Expression
	Assertion	axc15	$⊢ \neg \forall x x = y \to (x = y \to (φ \to \forall x (x = y \to φ)))$

Proof

Step	Hyp	Ref	Expression
1		ax6ev	$⊢ \exists z z = y$
2		dveeq2	$⊢ \neg \forall x x = y \to (z = y \to \forall x z = y)$
3		ax12v	$⊢ x = z \to (φ \to \forall x (x = z \to φ))$
4		equeuclr	$⊢ z = y \to (x = y \to x = z)$
5	4	sps	$⊢ \forall x z = y \to (x = y \to x = z)$
6	4	imim1d	$⊢ z = y \to ((x = z \to φ) \to (x = y \to φ))$
7	6	al2imi	$⊢ \forall x z = y \to (\forall x (x = z \to φ) \to \forall x (x = y \to φ))$
8	7	imim2d	$⊢ \forall x z = y \to ((φ \to \forall x (x = z \to φ)) \to (φ \to \forall x (x = y \to φ)))$
9	5 8	imim12d	$⊢ \forall x z = y \to ((x = z \to (φ \to \forall x (x = z \to φ))) \to (x = y \to (φ \to \forall x (x = y \to φ))))$
10	2 3 9	syl6mpi	$⊢ \neg \forall x x = y \to (z = y \to (x = y \to (φ \to \forall x (x = y \to φ))))$
11	10	exlimdv	$⊢ \neg \forall x x = y \to (\exists z z = y \to (x = y \to (φ \to \forall x (x = y \to φ))))$
12	1 11	mpi	$⊢ \neg \forall x x = y \to (x = y \to (φ \to \forall x (x = y \to φ)))$

Metamath Proof Explorer

Theorem axc15

Proof