wl-ax11-lem3

		Ref	Expression
	Assertion	wl-ax11-lem3	$⊢ \neg \forall x x = y \to Ⅎ x \forall u u = y$

Step	Hyp	Ref	Expression
1		nfna1	$⊢ Ⅎ x \neg \forall x x = y$
2		naev	$⊢ \neg \forall x x = y \to \neg \forall u u = x$
3		nfa1	$⊢ Ⅎ u \forall u u = y$
4		nfna1	$⊢ Ⅎ u \neg \forall u u = x$
5	3 4	nfan	$⊢ Ⅎ u (\forall u u = y \land \neg \forall u u = x)$
6		axc11n	$⊢ \forall x x = y \to \forall y y = x$
7		wl-aetr	$⊢ \forall y y = u \to (\forall y y = x \to \forall u u = x)$
8	6 7	syl5	$⊢ \forall y y = u \to (\forall x x = y \to \forall u u = x)$
9	8	aecoms	$⊢ \forall u u = y \to (\forall x x = y \to \forall u u = x)$
10	9	con3d	$⊢ \forall u u = y \to (\neg \forall u u = x \to \neg \forall x x = y)$
11	10	imdistani	$⊢ (\forall u u = y \land \neg \forall u u = x) \to (\forall u u = y \land \neg \forall x x = y)$
12		wl-ax11-lem2	$⊢ (\forall u u = y \land \neg \forall x x = y) \to \forall x u = y$
13	11 12	syl	$⊢ (\forall u u = y \land \neg \forall u u = x) \to \forall x u = y$
14	5 13	alrimi	$⊢ (\forall u u = y \land \neg \forall u u = x) \to \forall u \forall x u = y$
15	2 14	sylan2	$⊢ (\forall u u = y \land \neg \forall x x = y) \to \forall u \forall x u = y$
16	15	expcom	$⊢ \neg \forall x x = y \to (\forall u u = y \to \forall u \forall x u = y)$
17		ax-wl-11v	$⊢ \forall u \forall x u = y \to \forall x \forall u u = y$
18	16 17	syl6	$⊢ \neg \forall x x = y \to (\forall u u = y \to \forall x \forall u u = y)$
19	1 18	nf5d	$⊢ \neg \forall x x = y \to Ⅎ x \forall u u = y$

Metamath Proof Explorer