Theorem ax11el 2194

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

Assertion

Ref	Expression
ax11el	⊢ (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w))))

Proof of Theorem ax11el

Dummy variables u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.26 1593	. . 3 ⊢ (∀x(x = z ∧ x = w) ↔ (∀x x = z ∧ ∀x x = w))
2		elequ1 1713	. . . . . . . . 9 ⊢ (x = y → (x ∈ x ↔ y ∈ x))
3		elequ2 1715	. . . . . . . . 9 ⊢ (x = y → (y ∈ x ↔ y ∈ y))
4	2, 3	bitrd 244	. . . . . . . 8 ⊢ (x = y → (x ∈ x ↔ y ∈ y))
5	4	adantl 452	. . . . . . 7 ⊢ ((¬ ∀x x = y ∧ x = y) → (x ∈ x ↔ y ∈ y))
6		ax-17 1616	. . . . . . . . . 10 ⊢ (v ∈ v → ∀x v ∈ v)
7		ax-17 1616	. . . . . . . . . 10 ⊢ (y ∈ y → ∀v y ∈ y)
8		elequ1 1713	. . . . . . . . . . 11 ⊢ (v = y → (v ∈ v ↔ y ∈ v))
9		elequ2 1715	. . . . . . . . . . 11 ⊢ (v = y → (y ∈ v ↔ y ∈ y))
10	8, 9	bitrd 244	. . . . . . . . . 10 ⊢ (v = y → (v ∈ v ↔ y ∈ y))
11	6, 7, 10	dvelimf-o 2180	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (y ∈ y → ∀x y ∈ y))
12	4	biimprcd 216	. . . . . . . . . 10 ⊢ (y ∈ y → (x = y → x ∈ x))
13	12	alimi 1559	. . . . . . . . 9 ⊢ (∀x y ∈ y → ∀x(x = y → x ∈ x))
14	11, 13	syl6 29	. . . . . . . 8 ⊢ (¬ ∀x x = y → (y ∈ y → ∀x(x = y → x ∈ x)))
15	14	adantr 451	. . . . . . 7 ⊢ ((¬ ∀x x = y ∧ x = y) → (y ∈ y → ∀x(x = y → x ∈ x)))
16	5, 15	sylbid 206	. . . . . 6 ⊢ ((¬ ∀x x = y ∧ x = y) → (x ∈ x → ∀x(x = y → x ∈ x)))
17	16	adantl 452	. . . . 5 ⊢ ((∀x(x = z ∧ x = w) ∧ (¬ ∀x x = y ∧ x = y)) → (x ∈ x → ∀x(x = y → x ∈ x)))
18		elequ1 1713	. . . . . . . . 9 ⊢ (x = z → (x ∈ x ↔ z ∈ x))
19		elequ2 1715	. . . . . . . . 9 ⊢ (x = w → (z ∈ x ↔ z ∈ w))
20	18, 19	sylan9bb 680	. . . . . . . 8 ⊢ ((x = z ∧ x = w) → (x ∈ x ↔ z ∈ w))
21	20	sps-o 2159	. . . . . . 7 ⊢ (∀x(x = z ∧ x = w) → (x ∈ x ↔ z ∈ w))
22		nfa1-o 2166	. . . . . . . 8 ⊢ Ⅎx∀x(x = z ∧ x = w)
23	21	imbi2d 307	. . . . . . . 8 ⊢ (∀x(x = z ∧ x = w) → ((x = y → x ∈ x) ↔ (x = y → z ∈ w)))
24	22, 23	albid 1772	. . . . . . 7 ⊢ (∀x(x = z ∧ x = w) → (∀x(x = y → x ∈ x) ↔ ∀x(x = y → z ∈ w)))
25	21, 24	imbi12d 311	. . . . . 6 ⊢ (∀x(x = z ∧ x = w) → ((x ∈ x → ∀x(x = y → x ∈ x)) ↔ (z ∈ w → ∀x(x = y → z ∈ w))))
26	25	adantr 451	. . . . 5 ⊢ ((∀x(x = z ∧ x = w) ∧ (¬ ∀x x = y ∧ x = y)) → ((x ∈ x → ∀x(x = y → x ∈ x)) ↔ (z ∈ w → ∀x(x = y → z ∈ w))))
27	17, 26	mpbid 201	. . . 4 ⊢ ((∀x(x = z ∧ x = w) ∧ (¬ ∀x x = y ∧ x = y)) → (z ∈ w → ∀x(x = y → z ∈ w)))
28	27	exp32 588	. . 3 ⊢ (∀x(x = z ∧ x = w) → (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w)))))
29	1, 28	sylbir 204	. 2 ⊢ ((∀x x = z ∧ ∀x x = w) → (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w)))))
30		elequ1 1713	. . . . . . 7 ⊢ (x = y → (x ∈ w ↔ y ∈ w))
31	30	ad2antll 709	. . . . . 6 ⊢ ((¬ ∀x x = w ∧ (¬ ∀x x = y ∧ x = y)) → (x ∈ w ↔ y ∈ w))
32		ax-15 2143	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (¬ ∀x x = w → (y ∈ w → ∀x y ∈ w)))
33	32	impcom 419	. . . . . . . 8 ⊢ ((¬ ∀x x = w ∧ ¬ ∀x x = y) → (y ∈ w → ∀x y ∈ w))
34	33	adantrr 697	. . . . . . 7 ⊢ ((¬ ∀x x = w ∧ (¬ ∀x x = y ∧ x = y)) → (y ∈ w → ∀x y ∈ w))
35	30	biimprcd 216	. . . . . . . 8 ⊢ (y ∈ w → (x = y → x ∈ w))
36	35	alimi 1559	. . . . . . 7 ⊢ (∀x y ∈ w → ∀x(x = y → x ∈ w))
37	34, 36	syl6 29	. . . . . 6 ⊢ ((¬ ∀x x = w ∧ (¬ ∀x x = y ∧ x = y)) → (y ∈ w → ∀x(x = y → x ∈ w)))
38	31, 37	sylbid 206	. . . . 5 ⊢ ((¬ ∀x x = w ∧ (¬ ∀x x = y ∧ x = y)) → (x ∈ w → ∀x(x = y → x ∈ w)))
39	38	adantll 694	. . . 4 ⊢ (((∀x x = z ∧ ¬ ∀x x = w) ∧ (¬ ∀x x = y ∧ x = y)) → (x ∈ w → ∀x(x = y → x ∈ w)))
40		elequ1 1713	. . . . . . 7 ⊢ (x = z → (x ∈ w ↔ z ∈ w))
41	40	sps-o 2159	. . . . . 6 ⊢ (∀x x = z → (x ∈ w ↔ z ∈ w))
42	41	imbi2d 307	. . . . . . 7 ⊢ (∀x x = z → ((x = y → x ∈ w) ↔ (x = y → z ∈ w)))
43	42	dral2-o 2181	. . . . . 6 ⊢ (∀x x = z → (∀x(x = y → x ∈ w) ↔ ∀x(x = y → z ∈ w)))
44	41, 43	imbi12d 311	. . . . 5 ⊢ (∀x x = z → ((x ∈ w → ∀x(x = y → x ∈ w)) ↔ (z ∈ w → ∀x(x = y → z ∈ w))))
45	44	ad2antrr 706	. . . 4 ⊢ (((∀x x = z ∧ ¬ ∀x x = w) ∧ (¬ ∀x x = y ∧ x = y)) → ((x ∈ w → ∀x(x = y → x ∈ w)) ↔ (z ∈ w → ∀x(x = y → z ∈ w))))
46	39, 45	mpbid 201	. . 3 ⊢ (((∀x x = z ∧ ¬ ∀x x = w) ∧ (¬ ∀x x = y ∧ x = y)) → (z ∈ w → ∀x(x = y → z ∈ w)))
47	46	exp32 588	. 2 ⊢ ((∀x x = z ∧ ¬ ∀x x = w) → (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w)))))
48		elequ2 1715	. . . . . . 7 ⊢ (x = y → (z ∈ x ↔ z ∈ y))
49	48	ad2antll 709	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ x = y)) → (z ∈ x ↔ z ∈ y))
50		ax-15 2143	. . . . . . . . 9 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (z ∈ y → ∀x z ∈ y)))
51	50	imp 418	. . . . . . . 8 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (z ∈ y → ∀x z ∈ y))
52	51	adantrr 697	. . . . . . 7 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ x = y)) → (z ∈ y → ∀x z ∈ y))
53	48	biimprcd 216	. . . . . . . 8 ⊢ (z ∈ y → (x = y → z ∈ x))
54	53	alimi 1559	. . . . . . 7 ⊢ (∀x z ∈ y → ∀x(x = y → z ∈ x))
55	52, 54	syl6 29	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ x = y)) → (z ∈ y → ∀x(x = y → z ∈ x)))
56	49, 55	sylbid 206	. . . . 5 ⊢ ((¬ ∀x x = z ∧ (¬ ∀x x = y ∧ x = y)) → (z ∈ x → ∀x(x = y → z ∈ x)))
57	56	adantlr 695	. . . 4 ⊢ (((¬ ∀x x = z ∧ ∀x x = w) ∧ (¬ ∀x x = y ∧ x = y)) → (z ∈ x → ∀x(x = y → z ∈ x)))
58	19	sps-o 2159	. . . . . 6 ⊢ (∀x x = w → (z ∈ x ↔ z ∈ w))
59	58	imbi2d 307	. . . . . . 7 ⊢ (∀x x = w → ((x = y → z ∈ x) ↔ (x = y → z ∈ w)))
60	59	dral2-o 2181	. . . . . 6 ⊢ (∀x x = w → (∀x(x = y → z ∈ x) ↔ ∀x(x = y → z ∈ w)))
61	58, 60	imbi12d 311	. . . . 5 ⊢ (∀x x = w → ((z ∈ x → ∀x(x = y → z ∈ x)) ↔ (z ∈ w → ∀x(x = y → z ∈ w))))
62	61	ad2antlr 707	. . . 4 ⊢ (((¬ ∀x x = z ∧ ∀x x = w) ∧ (¬ ∀x x = y ∧ x = y)) → ((z ∈ x → ∀x(x = y → z ∈ x)) ↔ (z ∈ w → ∀x(x = y → z ∈ w))))
63	57, 62	mpbid 201	. . 3 ⊢ (((¬ ∀x x = z ∧ ∀x x = w) ∧ (¬ ∀x x = y ∧ x = y)) → (z ∈ w → ∀x(x = y → z ∈ w)))
64	63	exp32 588	. 2 ⊢ ((¬ ∀x x = z ∧ ∀x x = w) → (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w)))))
65		a9ev 1656	. . . . 5 ⊢ ∃u u = w
66		a9ev 1656	. . . . . . 7 ⊢ ∃v v = z
67		ax-1 6	. . . . . . . . . . 11 ⊢ (v ∈ u → (x = y → v ∈ u))
68	67	alrimiv 1631	. . . . . . . . . 10 ⊢ (v ∈ u → ∀x(x = y → v ∈ u))
69		elequ1 1713	. . . . . . . . . . . . 13 ⊢ (v = z → (v ∈ u ↔ z ∈ u))
70		elequ2 1715	. . . . . . . . . . . . 13 ⊢ (u = w → (z ∈ u ↔ z ∈ w))
71	69, 70	sylan9bb 680	. . . . . . . . . . . 12 ⊢ ((v = z ∧ u = w) → (v ∈ u ↔ z ∈ w))
72	71	adantl 452	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = z ∧ ¬ ∀x x = w) ∧ (v = z ∧ u = w)) → (v ∈ u ↔ z ∈ w))
73		dveeq2-o 2184	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀x x = z → (v = z → ∀x v = z))
74		dveeq2-o 2184	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀x x = w → (u = w → ∀x u = w))
75	73, 74	im2anan9 808	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = w) → ((v = z ∧ u = w) → (∀x v = z ∧ ∀x u = w)))
76	75	imp 418	. . . . . . . . . . . . 13 ⊢ (((¬ ∀x x = z ∧ ¬ ∀x x = w) ∧ (v = z ∧ u = w)) → (∀x v = z ∧ ∀x u = w))
77		19.26 1593	. . . . . . . . . . . . 13 ⊢ (∀x(v = z ∧ u = w) ↔ (∀x v = z ∧ ∀x u = w))
78	76, 77	sylibr 203	. . . . . . . . . . . 12 ⊢ (((¬ ∀x x = z ∧ ¬ ∀x x = w) ∧ (v = z ∧ u = w)) → ∀x(v = z ∧ u = w))
79		nfa1-o 2166	. . . . . . . . . . . . 13 ⊢ Ⅎx∀x(v = z ∧ u = w)
80	71	sps-o 2159	. . . . . . . . . . . . . 14 ⊢ (∀x(v = z ∧ u = w) → (v ∈ u ↔ z ∈ w))
81	80	imbi2d 307	. . . . . . . . . . . . 13 ⊢ (∀x(v = z ∧ u = w) → ((x = y → v ∈ u) ↔ (x = y → z ∈ w)))
82	79, 81	albid 1772	. . . . . . . . . . . 12 ⊢ (∀x(v = z ∧ u = w) → (∀x(x = y → v ∈ u) ↔ ∀x(x = y → z ∈ w)))
83	78, 82	syl 15	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = z ∧ ¬ ∀x x = w) ∧ (v = z ∧ u = w)) → (∀x(x = y → v ∈ u) ↔ ∀x(x = y → z ∈ w)))
84	72, 83	imbi12d 311	. . . . . . . . . 10 ⊢ (((¬ ∀x x = z ∧ ¬ ∀x x = w) ∧ (v = z ∧ u = w)) → ((v ∈ u → ∀x(x = y → v ∈ u)) ↔ (z ∈ w → ∀x(x = y → z ∈ w))))
85	68, 84	mpbii 202	. . . . . . . . 9 ⊢ (((¬ ∀x x = z ∧ ¬ ∀x x = w) ∧ (v = z ∧ u = w)) → (z ∈ w → ∀x(x = y → z ∈ w)))
86	85	exp32 588	. . . . . . . 8 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = w) → (v = z → (u = w → (z ∈ w → ∀x(x = y → z ∈ w)))))
87	86	exlimdv 1636	. . . . . . 7 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = w) → (∃v v = z → (u = w → (z ∈ w → ∀x(x = y → z ∈ w)))))
88	66, 87	mpi 16	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = w) → (u = w → (z ∈ w → ∀x(x = y → z ∈ w))))
89	88	exlimdv 1636	. . . . 5 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = w) → (∃u u = w → (z ∈ w → ∀x(x = y → z ∈ w))))
90	65, 89	mpi 16	. . . 4 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = w) → (z ∈ w → ∀x(x = y → z ∈ w)))
91	90	a1d 22	. . 3 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = w) → (x = y → (z ∈ w → ∀x(x = y → z ∈ w))))
92	91	a1d 22	. 2 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = w) → (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w)))))
93	29, 47, 64, 92	4cases 915	1 ⊢ (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-4 2135  ax-5o 2136  ax-6o 2137  ax-10o 2139  ax-12o 2142  ax-15 2143

This proof depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is used by: (None)