ax12eq

Description: Basis step for constructing a substitution instance of ax-c15 without using ax-c15 . Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	ax12eq	$⊢ \neg \forall x x = y \to (x = y \to (z = w \to \forall x (x = y \to z = w)))$

Proof

Step	Hyp	Ref	Expression
1		19.26	$⊢ \forall x (x = z \land x = w) \leftrightarrow (\forall x x = z \land \forall x x = w)$
2		equid	$⊢ x = x$
3	2	a1i	$⊢ x = y \to x = x$
4	3	ax-gen	$⊢ \forall x (x = y \to x = x)$
5	4	a1i	$⊢ x = x \to \forall x (x = y \to x = x)$
6		equequ1	$⊢ x = z \to (x = x \leftrightarrow z = x)$
7		equequ2	$⊢ x = w \to (z = x \leftrightarrow z = w)$
8	6 7	sylan9bb	$⊢ (x = z \land x = w) \to (x = x \leftrightarrow z = w)$
9	8	sps-o	$⊢ \forall x (x = z \land x = w) \to (x = x \leftrightarrow z = w)$
10		nfa1-o	$⊢ Ⅎ x \forall x (x = z \land x = w)$
11	9	imbi2d	$⊢ \forall x (x = z \land x = w) \to ((x = y \to x = x) \leftrightarrow (x = y \to z = w))$
12	10 11	albid	$⊢ \forall x (x = z \land x = w) \to (\forall x (x = y \to x = x) \leftrightarrow \forall x (x = y \to z = w))$
13	9 12	imbi12d	$⊢ \forall x (x = z \land x = w) \to ((x = x \to \forall x (x = y \to x = x)) \leftrightarrow (z = w \to \forall x (x = y \to z = w)))$
14	13	adantr	$⊢ (\forall x (x = z \land x = w) \land (\neg \forall x x = y \land x = y)) \to ((x = x \to \forall x (x = y \to x = x)) \leftrightarrow (z = w \to \forall x (x = y \to z = w)))$
15	5 14	mpbii	$⊢ (\forall x (x = z \land x = w) \land (\neg \forall x x = y \land x = y)) \to (z = w \to \forall x (x = y \to z = w))$
16	15	exp32	$⊢ \forall x (x = z \land x = w) \to (\neg \forall x x = y \to (x = y \to (z = w \to \forall x (x = y \to z = w))))$
17	1 16	sylbir	$⊢ (\forall x x = z \land \forall x x = w) \to (\neg \forall x x = y \to (x = y \to (z = w \to \forall x (x = y \to z = w))))$
18		equequ1	$⊢ x = y \to (x = w \leftrightarrow y = w)$
19	18	ad2antll	$⊢ (\neg \forall x x = w \land (\neg \forall x x = y \land x = y)) \to (x = w \leftrightarrow y = w)$
20		axc9	$⊢ \neg \forall x x = y \to (\neg \forall x x = w \to (y = w \to \forall x y = w))$
21	20	impcom	$⊢ (\neg \forall x x = w \land \neg \forall x x = y) \to (y = w \to \forall x y = w)$
22	21	adantrr	$⊢ (\neg \forall x x = w \land (\neg \forall x x = y \land x = y)) \to (y = w \to \forall x y = w)$
23		equtrr	$⊢ y = w \to (x = y \to x = w)$
24	23	alimi	$⊢ \forall x y = w \to \forall x (x = y \to x = w)$
25	22 24	syl6	$⊢ (\neg \forall x x = w \land (\neg \forall x x = y \land x = y)) \to (y = w \to \forall x (x = y \to x = w))$
26	19 25	sylbid	$⊢ (\neg \forall x x = w \land (\neg \forall x x = y \land x = y)) \to (x = w \to \forall x (x = y \to x = w))$
27	26	adantll	$⊢ ((\forall x x = z \land \neg \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to (x = w \to \forall x (x = y \to x = w))$
28		equequ1	$⊢ x = z \to (x = w \leftrightarrow z = w)$
29	28	sps-o	$⊢ \forall x x = z \to (x = w \leftrightarrow z = w)$
30	29	imbi2d	$⊢ \forall x x = z \to ((x = y \to x = w) \leftrightarrow (x = y \to z = w))$
31	30	dral2-o	$⊢ \forall x x = z \to (\forall x (x = y \to x = w) \leftrightarrow \forall x (x = y \to z = w))$
32	29 31	imbi12d	$⊢ \forall x x = z \to ((x = w \to \forall x (x = y \to x = w)) \leftrightarrow (z = w \to \forall x (x = y \to z = w)))$
33	32	ad2antrr	$⊢ ((\forall x x = z \land \neg \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to ((x = w \to \forall x (x = y \to x = w)) \leftrightarrow (z = w \to \forall x (x = y \to z = w)))$
34	27 33	mpbid	$⊢ ((\forall x x = z \land \neg \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to (z = w \to \forall x (x = y \to z = w))$
35	34	exp32	$⊢ (\forall x x = z \land \neg \forall x x = w) \to (\neg \forall x x = y \to (x = y \to (z = w \to \forall x (x = y \to z = w))))$
36		equequ2	$⊢ x = y \to (z = x \leftrightarrow z = y)$
37	36	ad2antll	$⊢ (\neg \forall x x = z \land (\neg \forall x x = y \land x = y)) \to (z = x \leftrightarrow z = y)$
38		axc9	$⊢ \neg \forall x x = z \to (\neg \forall x x = y \to (z = y \to \forall x z = y))$
39	38	imp	$⊢ (\neg \forall x x = z \land \neg \forall x x = y) \to (z = y \to \forall x z = y)$
40	39	adantrr	$⊢ (\neg \forall x x = z \land (\neg \forall x x = y \land x = y)) \to (z = y \to \forall x z = y)$
41	36	biimprcd	$⊢ z = y \to (x = y \to z = x)$
42	41	alimi	$⊢ \forall x z = y \to \forall x (x = y \to z = x)$
43	40 42	syl6	$⊢ (\neg \forall x x = z \land (\neg \forall x x = y \land x = y)) \to (z = y \to \forall x (x = y \to z = x))$
44	37 43	sylbid	$⊢ (\neg \forall x x = z \land (\neg \forall x x = y \land x = y)) \to (z = x \to \forall x (x = y \to z = x))$
45	44	adantlr	$⊢ ((\neg \forall x x = z \land \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to (z = x \to \forall x (x = y \to z = x))$
46	7	sps-o	$⊢ \forall x x = w \to (z = x \leftrightarrow z = w)$
47	46	imbi2d	$⊢ \forall x x = w \to ((x = y \to z = x) \leftrightarrow (x = y \to z = w))$
48	47	dral2-o	$⊢ \forall x x = w \to (\forall x (x = y \to z = x) \leftrightarrow \forall x (x = y \to z = w))$
49	46 48	imbi12d	$⊢ \forall x x = w \to ((z = x \to \forall x (x = y \to z = x)) \leftrightarrow (z = w \to \forall x (x = y \to z = w)))$
50	49	ad2antlr	$⊢ ((\neg \forall x x = z \land \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to ((z = x \to \forall x (x = y \to z = x)) \leftrightarrow (z = w \to \forall x (x = y \to z = w)))$
51	45 50	mpbid	$⊢ ((\neg \forall x x = z \land \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to (z = w \to \forall x (x = y \to z = w))$
52	51	exp32	$⊢ (\neg \forall x x = z \land \forall x x = w) \to (\neg \forall x x = y \to (x = y \to (z = w \to \forall x (x = y \to z = w))))$
53		ax6ev	$⊢ \exists u u = w$
54		ax6ev	$⊢ \exists v v = z$
55		ax-1	$⊢ v = u \to (x = y \to v = u)$
56	55	alrimiv	$⊢ v = u \to \forall x (x = y \to v = u)$
57		equequ1	$⊢ v = z \to (v = u \leftrightarrow z = u)$
58		equequ2	$⊢ u = w \to (z = u \leftrightarrow z = w)$
59	57 58	sylan9bb	$⊢ (v = z \land u = w) \to (v = u \leftrightarrow z = w)$
60	59	adantl	$⊢ ((\neg \forall x x = z \land \neg \forall x x = w) \land (v = z \land u = w)) \to (v = u \leftrightarrow z = w)$
61		dveeq2-o	$⊢ \neg \forall x x = z \to (v = z \to \forall x v = z)$
62		dveeq2-o	$⊢ \neg \forall x x = w \to (u = w \to \forall x u = w)$
63	61 62	im2anan9	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to ((v = z \land u = w) \to (\forall x v = z \land \forall x u = w))$
64	63	imp	$⊢ ((\neg \forall x x = z \land \neg \forall x x = w) \land (v = z \land u = w)) \to (\forall x v = z \land \forall x u = w)$
65		19.26	$⊢ \forall x (v = z \land u = w) \leftrightarrow (\forall x v = z \land \forall x u = w)$
66	64 65	sylibr	$⊢ ((\neg \forall x x = z \land \neg \forall x x = w) \land (v = z \land u = w)) \to \forall x (v = z \land u = w)$
67		nfa1-o	$⊢ Ⅎ x \forall x (v = z \land u = w)$
68	59	sps-o	$⊢ \forall x (v = z \land u = w) \to (v = u \leftrightarrow z = w)$
69	68	imbi2d	$⊢ \forall x (v = z \land u = w) \to ((x = y \to v = u) \leftrightarrow (x = y \to z = w))$
70	67 69	albid	$⊢ \forall x (v = z \land u = w) \to (\forall x (x = y \to v = u) \leftrightarrow \forall x (x = y \to z = w))$
71	66 70	syl	$⊢ ((\neg \forall x x = z \land \neg \forall x x = w) \land (v = z \land u = w)) \to (\forall x (x = y \to v = u) \leftrightarrow \forall x (x = y \to z = w))$
72	60 71	imbi12d	$⊢ ((\neg \forall x x = z \land \neg \forall x x = w) \land (v = z \land u = w)) \to ((v = u \to \forall x (x = y \to v = u)) \leftrightarrow (z = w \to \forall x (x = y \to z = w)))$
73	56 72	mpbii	$⊢ ((\neg \forall x x = z \land \neg \forall x x = w) \land (v = z \land u = w)) \to (z = w \to \forall x (x = y \to z = w))$
74	73	exp32	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (v = z \to (u = w \to (z = w \to \forall x (x = y \to z = w))))$
75	74	exlimdv	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (\exists v v = z \to (u = w \to (z = w \to \forall x (x = y \to z = w))))$
76	54 75	mpi	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (u = w \to (z = w \to \forall x (x = y \to z = w)))$
77	76	exlimdv	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (\exists u u = w \to (z = w \to \forall x (x = y \to z = w)))$
78	53 77	mpi	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (z = w \to \forall x (x = y \to z = w))$
79	78	a1d	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (x = y \to (z = w \to \forall x (x = y \to z = w)))$
80	79	a1d	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (\neg \forall x x = y \to (x = y \to (z = w \to \forall x (x = y \to z = w))))$
81	17 35 52 80	4cases	$⊢ \neg \forall x x = y \to (x = y \to (z = w \to \forall x (x = y \to z = w)))$

Metamath Proof Explorer

Theorem ax12eq

Proof