ax12el

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

		Ref	Expression
	Assertion	ax12el	$⊢ \neg \forall x x = y \to (x = y \to (z \in w \to \forall x (x = y \to z \in 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		elequ1	$⊢ x = y \to (x \in x \leftrightarrow y \in x)$
3		elequ2	$⊢ x = y \to (y \in x \leftrightarrow y \in y)$
4	2 3	bitrd	$⊢ x = y \to (x \in x \leftrightarrow y \in y)$
5	4	adantl	$⊢ (\neg \forall x x = y \land x = y) \to (x \in x \leftrightarrow y \in y)$
6		ax-5	$⊢ v \in v \to \forall x v \in v$
7		ax-5	$⊢ y \in y \to \forall v y \in y$
8		elequ1	$⊢ v = y \to (v \in v \leftrightarrow y \in v)$
9		elequ2	$⊢ v = y \to (y \in v \leftrightarrow y \in y)$
10	8 9	bitrd	$⊢ v = y \to (v \in v \leftrightarrow y \in y)$
11	6 7 10	dvelimf-o	$⊢ \neg \forall x x = y \to (y \in y \to \forall x y \in y)$
12	4	biimprcd	$⊢ y \in y \to (x = y \to x \in x)$
13	12	alimi	$⊢ \forall x y \in y \to \forall x (x = y \to x \in x)$
14	11 13	syl6	$⊢ \neg \forall x x = y \to (y \in y \to \forall x (x = y \to x \in x))$
15	14	adantr	$⊢ (\neg \forall x x = y \land x = y) \to (y \in y \to \forall x (x = y \to x \in x))$
16	5 15	sylbid	$⊢ (\neg \forall x x = y \land x = y) \to (x \in x \to \forall x (x = y \to x \in x))$
17	16	adantl	$⊢ (\forall x (x = z \land x = w) \land (\neg \forall x x = y \land x = y)) \to (x \in x \to \forall x (x = y \to x \in x))$
18		elequ1	$⊢ x = z \to (x \in x \leftrightarrow z \in x)$
19		elequ2	$⊢ x = w \to (z \in x \leftrightarrow z \in w)$
20	18 19	sylan9bb	$⊢ (x = z \land x = w) \to (x \in x \leftrightarrow z \in w)$
21	20	sps-o	$⊢ \forall x (x = z \land x = w) \to (x \in x \leftrightarrow z \in w)$
22		nfa1-o	$⊢ Ⅎ x \forall x (x = z \land x = w)$
23	21	imbi2d	$⊢ \forall x (x = z \land x = w) \to ((x = y \to x \in x) \leftrightarrow (x = y \to z \in w))$
24	22 23	albid	$⊢ \forall x (x = z \land x = w) \to (\forall x (x = y \to x \in x) \leftrightarrow \forall x (x = y \to z \in w))$
25	21 24	imbi12d	$⊢ \forall x (x = z \land x = w) \to ((x \in x \to \forall x (x = y \to x \in x)) \leftrightarrow (z \in w \to \forall x (x = y \to z \in w)))$
26	25	adantr	$⊢ (\forall x (x = z \land x = w) \land (\neg \forall x x = y \land x = y)) \to ((x \in x \to \forall x (x = y \to x \in x)) \leftrightarrow (z \in w \to \forall x (x = y \to z \in w)))$
27	17 26	mpbid	$⊢ (\forall x (x = z \land x = w) \land (\neg \forall x x = y \land x = y)) \to (z \in w \to \forall x (x = y \to z \in w))$
28	27	exp32	$⊢ \forall x (x = z \land x = w) \to (\neg \forall x x = y \to (x = y \to (z \in w \to \forall x (x = y \to z \in w))))$
29	1 28	sylbir	$⊢ (\forall x x = z \land \forall x x = w) \to (\neg \forall x x = y \to (x = y \to (z \in w \to \forall x (x = y \to z \in w))))$
30		elequ1	$⊢ x = y \to (x \in w \leftrightarrow y \in w)$
31	30	ad2antll	$⊢ (\neg \forall x x = w \land (\neg \forall x x = y \land x = y)) \to (x \in w \leftrightarrow y \in w)$
32		ax-c14	$⊢ \neg \forall x x = y \to (\neg \forall x x = w \to (y \in w \to \forall x y \in w))$
33	32	impcom	$⊢ (\neg \forall x x = w \land \neg \forall x x = y) \to (y \in w \to \forall x y \in w)$
34	33	adantrr	$⊢ (\neg \forall x x = w \land (\neg \forall x x = y \land x = y)) \to (y \in w \to \forall x y \in w)$
35	30	biimprcd	$⊢ y \in w \to (x = y \to x \in w)$
36	35	alimi	$⊢ \forall x y \in w \to \forall x (x = y \to x \in w)$
37	34 36	syl6	$⊢ (\neg \forall x x = w \land (\neg \forall x x = y \land x = y)) \to (y \in w \to \forall x (x = y \to x \in w))$
38	31 37	sylbid	$⊢ (\neg \forall x x = w \land (\neg \forall x x = y \land x = y)) \to (x \in w \to \forall x (x = y \to x \in w))$
39	38	adantll	$⊢ ((\forall x x = z \land \neg \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to (x \in w \to \forall x (x = y \to x \in w))$
40		elequ1	$⊢ x = z \to (x \in w \leftrightarrow z \in w)$
41	40	sps-o	$⊢ \forall x x = z \to (x \in w \leftrightarrow z \in w)$
42	41	imbi2d	$⊢ \forall x x = z \to ((x = y \to x \in w) \leftrightarrow (x = y \to z \in w))$
43	42	dral2-o	$⊢ \forall x x = z \to (\forall x (x = y \to x \in w) \leftrightarrow \forall x (x = y \to z \in w))$
44	41 43	imbi12d	$⊢ \forall x x = z \to ((x \in w \to \forall x (x = y \to x \in w)) \leftrightarrow (z \in w \to \forall x (x = y \to z \in w)))$
45	44	ad2antrr	$⊢ ((\forall x x = z \land \neg \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to ((x \in w \to \forall x (x = y \to x \in w)) \leftrightarrow (z \in w \to \forall x (x = y \to z \in w)))$
46	39 45	mpbid	$⊢ ((\forall x x = z \land \neg \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to (z \in w \to \forall x (x = y \to z \in w))$
47	46	exp32	$⊢ (\forall x x = z \land \neg \forall x x = w) \to (\neg \forall x x = y \to (x = y \to (z \in w \to \forall x (x = y \to z \in w))))$
48		elequ2	$⊢ x = y \to (z \in x \leftrightarrow z \in y)$
49	48	ad2antll	$⊢ (\neg \forall x x = z \land (\neg \forall x x = y \land x = y)) \to (z \in x \leftrightarrow z \in y)$
50		ax-c14	$⊢ \neg \forall x x = z \to (\neg \forall x x = y \to (z \in y \to \forall x z \in y))$
51	50	imp	$⊢ (\neg \forall x x = z \land \neg \forall x x = y) \to (z \in y \to \forall x z \in y)$
52	51	adantrr	$⊢ (\neg \forall x x = z \land (\neg \forall x x = y \land x = y)) \to (z \in y \to \forall x z \in y)$
53	48	biimprcd	$⊢ z \in y \to (x = y \to z \in x)$
54	53	alimi	$⊢ \forall x z \in y \to \forall x (x = y \to z \in x)$
55	52 54	syl6	$⊢ (\neg \forall x x = z \land (\neg \forall x x = y \land x = y)) \to (z \in y \to \forall x (x = y \to z \in x))$
56	49 55	sylbid	$⊢ (\neg \forall x x = z \land (\neg \forall x x = y \land x = y)) \to (z \in x \to \forall x (x = y \to z \in x))$
57	56	adantlr	$⊢ ((\neg \forall x x = z \land \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to (z \in x \to \forall x (x = y \to z \in x))$
58	19	sps-o	$⊢ \forall x x = w \to (z \in x \leftrightarrow z \in w)$
59	58	imbi2d	$⊢ \forall x x = w \to ((x = y \to z \in x) \leftrightarrow (x = y \to z \in w))$
60	59	dral2-o	$⊢ \forall x x = w \to (\forall x (x = y \to z \in x) \leftrightarrow \forall x (x = y \to z \in w))$
61	58 60	imbi12d	$⊢ \forall x x = w \to ((z \in x \to \forall x (x = y \to z \in x)) \leftrightarrow (z \in w \to \forall x (x = y \to z \in w)))$
62	61	ad2antlr	$⊢ ((\neg \forall x x = z \land \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to ((z \in x \to \forall x (x = y \to z \in x)) \leftrightarrow (z \in w \to \forall x (x = y \to z \in w)))$
63	57 62	mpbid	$⊢ ((\neg \forall x x = z \land \forall x x = w) \land (\neg \forall x x = y \land x = y)) \to (z \in w \to \forall x (x = y \to z \in w))$
64	63	exp32	$⊢ (\neg \forall x x = z \land \forall x x = w) \to (\neg \forall x x = y \to (x = y \to (z \in w \to \forall x (x = y \to z \in w))))$
65		ax6ev	$⊢ \exists u u = w$
66		ax6ev	$⊢ \exists v v = z$
67		ax-1	$⊢ v \in u \to (x = y \to v \in u)$
68	67	alrimiv	$⊢ v \in u \to \forall x (x = y \to v \in u)$
69		elequ1	$⊢ v = z \to (v \in u \leftrightarrow z \in u)$
70		elequ2	$⊢ u = w \to (z \in u \leftrightarrow z \in w)$
71	69 70	sylan9bb	$⊢ (v = z \land u = w) \to (v \in u \leftrightarrow z \in w)$
72	71	adantl	$⊢ ((\neg \forall x x = z \land \neg \forall x x = w) \land (v = z \land u = w)) \to (v \in u \leftrightarrow z \in w)$
73		dveeq2-o	$⊢ \neg \forall x x = z \to (v = z \to \forall x v = z)$
74		dveeq2-o	$⊢ \neg \forall x x = w \to (u = w \to \forall x u = w)$
75	73 74	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))$
76	75	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)$
77		19.26	$⊢ \forall x (v = z \land u = w) \leftrightarrow (\forall x v = z \land \forall x u = w)$
78	76 77	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)$
79		nfa1-o	$⊢ Ⅎ x \forall x (v = z \land u = w)$
80	71	sps-o	$⊢ \forall x (v = z \land u = w) \to (v \in u \leftrightarrow z \in w)$
81	80	imbi2d	$⊢ \forall x (v = z \land u = w) \to ((x = y \to v \in u) \leftrightarrow (x = y \to z \in w))$
82	79 81	albid	$⊢ \forall x (v = z \land u = w) \to (\forall x (x = y \to v \in u) \leftrightarrow \forall x (x = y \to z \in w))$
83	78 82	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 \in u) \leftrightarrow \forall x (x = y \to z \in w))$
84	72 83	imbi12d	$⊢ ((\neg \forall x x = z \land \neg \forall x x = w) \land (v = z \land u = w)) \to ((v \in u \to \forall x (x = y \to v \in u)) \leftrightarrow (z \in w \to \forall x (x = y \to z \in w)))$
85	68 84	mpbii	$⊢ ((\neg \forall x x = z \land \neg \forall x x = w) \land (v = z \land u = w)) \to (z \in w \to \forall x (x = y \to z \in w))$
86	85	exp32	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (v = z \to (u = w \to (z \in w \to \forall x (x = y \to z \in w))))$
87	86	exlimdv	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (\exists v v = z \to (u = w \to (z \in w \to \forall x (x = y \to z \in w))))$
88	66 87	mpi	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (u = w \to (z \in w \to \forall x (x = y \to z \in w)))$
89	88	exlimdv	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (\exists u u = w \to (z \in w \to \forall x (x = y \to z \in w)))$
90	65 89	mpi	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (z \in w \to \forall x (x = y \to z \in w))$
91	90	a1d	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (x = y \to (z \in w \to \forall x (x = y \to z \in w)))$
92	91	a1d	$⊢ (\neg \forall x x = z \land \neg \forall x x = w) \to (\neg \forall x x = y \to (x = y \to (z \in w \to \forall x (x = y \to z \in w))))$
93	29 47 64 92	4cases	$⊢ \neg \forall x x = y \to (x = y \to (z \in w \to \forall x (x = y \to z \in w)))$

Metamath Proof Explorer

Theorem ax12el

Proof