Theorem ax11el 1364

Description: Basis step for constructing a substitution instance of ax-11o 1218 without using ax-11o 1218. Atomic formula for membership predicate.

Assertion

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

Proof of Theorem ax11el

Step	Hyp	Ref	Expression
1		19.26 1067	. . 3 ⊢ (∀x(x = z ⋀ x = w) ↔ (∀x x = z ⋀ ∀x x = w))
2		elequ1 1136	. . . . . . . . 9 ⊢ (x = y → (x ∈ x ↔ y ∈ x))
3		elequ2 1137	. . . . . . . . 9 ⊢ (x = y → (y ∈ x ↔ y ∈ y))
4	2, 3	bitrd 528	. . . . . . . 8 ⊢ (x = y → (x ∈ x ↔ y ∈ y))
5	4	adantl 388	. . . . . . 7 ⊢ ((¬ ∀x x = y ⋀ x = y) → (x ∈ x ↔ y ∈ y))
6		ax-17 971	. . . . . . . . . 10 ⊢ (v ∈ v → ∀x v ∈ v)
7		ax-17 971	. . . . . . . . . 10 ⊢ (y ∈ y → ∀v y ∈ y)
8		elequ1 1136	. . . . . . . . . . 11 ⊢ (v = y → (v ∈ v ↔ y ∈ v))
9		elequ2 1137	. . . . . . . . . . 11 ⊢ (v = y → (y ∈ v ↔ y ∈ y))
10	8, 9	bitrd 528	. . . . . . . . . 10 ⊢ (v = y → (v ∈ v ↔ y ∈ y))
11	6, 7, 10	dvelimfALT 1153	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (y ∈ y → ∀x y ∈ y))
12	4	biimprcd 156	. . . . . . . . . 10 ⊢ (y ∈ y → (x = y → x ∈ x))
13	12	19.20i 992	. . . . . . . . 9 ⊢ (∀x y ∈ y → ∀x(x = y → x ∈ x))
14	11, 13	syl6 22	. . . . . . . 8 ⊢ (¬ ∀x x = y → (y ∈ y → ∀x(x = y → x ∈ x)))
15	14	adantr 389	. . . . . . 7 ⊢ ((¬ ∀x x = y ⋀ x = y) → (y ∈ y → ∀x(x = y → x ∈ x)))
16	5, 15	sylbid 203	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ x = y) → (x ∈ x → ∀x(x = y → x ∈ x)))
17	16	adantl 388	. . . . 5 ⊢ ((∀x(x = z ⋀ x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (x ∈ x → ∀x(x = y → x ∈ x)))
18		elequ1 1136	. . . . . . . . 9 ⊢ (x = z → (x ∈ x ↔ z ∈ x))
19		elequ2 1137	. . . . . . . . 9 ⊢ (x = w → (z ∈ x ↔ z ∈ w))
20	18, 19	sylan9bb 540	. . . . . . . 8 ⊢ ((x = z ⋀ x = w) → (x ∈ x ↔ z ∈ w))
21	20	a4s 984	. . . . . . 7 ⊢ (∀x(x = z ⋀ x = w) → (x ∈ x ↔ z ∈ w))
22		hba1 1003	. . . . . . . 8 ⊢ (∀x(x = z ⋀ x = w) → ∀x∀x(x = z ⋀ x = w))
23	21	imbi2d 612	. . . . . . . 8 ⊢ (∀x(x = z ⋀ x = w) → ((x = y → x ∈ x) ↔ (x = y → z ∈ w)))
24	22, 23	albid 1104	. . . . . . 7 ⊢ (∀x(x = z ⋀ x = w) → (∀x(x = y → x ∈ x) ↔ ∀x(x = y → z ∈ w)))
25	21, 24	imbi12d 626	. . . . . 6 ⊢ (∀x(x = z ⋀ x = w) → ((x ∈ x → ∀x(x = y → x ∈ x)) ↔ (z ∈ w → ∀x(x = y → z ∈ w))))
26	25	adantr 389	. . . . 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 195	. . . 4 ⊢ ((∀x(x = z ⋀ x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (z ∈ w → ∀x(x = y → z ∈ w)))
28	27	exp32 377	. . 3 ⊢ (∀x(x = z ⋀ x = w) → (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w)))))
29	1, 28	sylbir 201	. 2 ⊢ ((∀x x = z ⋀ ∀x x = w) → (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w)))))
30		elequ1 1136	. . . . . . 7 ⊢ (x = y → (x ∈ w ↔ y ∈ w))
31	30	ad2antll 407	. . . . . 6 ⊢ ((¬ ∀x x = w ⋀ (¬ ∀x x = y ⋀ x = y)) → (x ∈ w ↔ y ∈ w))
32		ax-15 1360	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (¬ ∀x x = w → (y ∈ w → ∀x y ∈ w)))
33	32	impcom 351	. . . . . . . 8 ⊢ ((¬ ∀x x = w ⋀ ¬ ∀x x = y) → (y ∈ w → ∀x y ∈ w))
34	33	adantrr 395	. . . . . . 7 ⊢ ((¬ ∀x x = w ⋀ (¬ ∀x x = y ⋀ x = y)) → (y ∈ w → ∀x y ∈ w))
35	30	biimprcd 156	. . . . . . . 8 ⊢ (y ∈ w → (x = y → x ∈ w))
36	35	19.20i 992	. . . . . . 7 ⊢ (∀x y ∈ w → ∀x(x = y → x ∈ w))
37	34, 36	syl6 22	. . . . . 6 ⊢ ((¬ ∀x x = w ⋀ (¬ ∀x x = y ⋀ x = y)) → (y ∈ w → ∀x(x = y → x ∈ w)))
38	31, 37	sylbid 203	. . . . 5 ⊢ ((¬ ∀x x = w ⋀ (¬ ∀x x = y ⋀ x = y)) → (x ∈ w → ∀x(x = y → x ∈ w)))
39	38	adantll 392	. . . 4 ⊢ (((∀x x = z ⋀ ¬ ∀x x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (x ∈ w → ∀x(x = y → x ∈ w)))
40		elequ1 1136	. . . . . . 7 ⊢ (x = z → (x ∈ w ↔ z ∈ w))
41	40	a4s 984	. . . . . 6 ⊢ (∀x x = z → (x ∈ w ↔ z ∈ w))
42	41	imbi2d 612	. . . . . . 7 ⊢ (∀x x = z → ((x = y → x ∈ w) ↔ (x = y → z ∈ w)))
43	42	dral2 1155	. . . . . 6 ⊢ (∀x x = z → (∀x(x = y → x ∈ w) ↔ ∀x(x = y → z ∈ w)))
44	41, 43	imbi12d 626	. . . . 5 ⊢ (∀x x = z → ((x ∈ w → ∀x(x = y → x ∈ w)) ↔ (z ∈ w → ∀x(x = y → z ∈ w))))
45	44	ad2antrr 404	. . . 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 195	. . 3 ⊢ (((∀x x = z ⋀ ¬ ∀x x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (z ∈ w → ∀x(x = y → z ∈ w)))
47	46	exp32 377	. 2 ⊢ ((∀x x = z ⋀ ¬ ∀x x = w) → (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w)))))
48		elequ2 1137	. . . . . . 7 ⊢ (x = y → (z ∈ x ↔ z ∈ y))
49	48	ad2antll 407	. . . . . 6 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ x = y)) → (z ∈ x ↔ z ∈ y))
50		ax-15 1360	. . . . . . . . 9 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (z ∈ y → ∀x z ∈ y)))
51	50	imp 350	. . . . . . . 8 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → (z ∈ y → ∀x z ∈ y))
52	51	adantrr 395	. . . . . . 7 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ x = y)) → (z ∈ y → ∀x z ∈ y))
53	48	biimprcd 156	. . . . . . . 8 ⊢ (z ∈ y → (x = y → z ∈ x))
54	53	19.20i 992	. . . . . . 7 ⊢ (∀x z ∈ y → ∀x(x = y → z ∈ x))
55	52, 54	syl6 22	. . . . . 6 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ x = y)) → (z ∈ y → ∀x(x = y → z ∈ x)))
56	49, 55	sylbid 203	. . . . 5 ⊢ ((¬ ∀x x = z ⋀ (¬ ∀x x = y ⋀ x = y)) → (z ∈ x → ∀x(x = y → z ∈ x)))
57	56	adantlr 393	. . . 4 ⊢ (((¬ ∀x x = z ⋀ ∀x x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (z ∈ x → ∀x(x = y → z ∈ x)))
58	19	a4s 984	. . . . . 6 ⊢ (∀x x = w → (z ∈ x ↔ z ∈ w))
59	58	imbi2d 612	. . . . . . 7 ⊢ (∀x x = w → ((x = y → z ∈ x) ↔ (x = y → z ∈ w)))
60	59	dral2 1155	. . . . . 6 ⊢ (∀x x = w → (∀x(x = y → z ∈ x) ↔ ∀x(x = y → z ∈ w)))
61	58, 60	imbi12d 626	. . . . 5 ⊢ (∀x x = w → ((z ∈ x → ∀x(x = y → z ∈ x)) ↔ (z ∈ w → ∀x(x = y → z ∈ w))))
62	61	ad2antlr 405	. . . 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 195	. . 3 ⊢ (((¬ ∀x x = z ⋀ ∀x x = w) ⋀ (¬ ∀x x = y ⋀ x = y)) → (z ∈ w → ∀x(x = y → z ∈ w)))
64	63	exp32 377	. 2 ⊢ ((¬ ∀x x = z ⋀ ∀x x = w) → (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w)))))
65		a9e 1125	. . . . 5 ⊢ ∃u u = w
66		a9e 1125	. . . . . . 7 ⊢ ∃v v = z
67		ax-1 4	. . . . . . . . . . 11 ⊢ (v ∈ u → (x = y → v ∈ u))
68	67	19.21aiv 1286	. . . . . . . . . 10 ⊢ (v ∈ u → ∀x(x = y → v ∈ u))
69		elequ1 1136	. . . . . . . . . . . . 13 ⊢ (v = z → (v ∈ u ↔ z ∈ u))
70		elequ2 1137	. . . . . . . . . . . . 13 ⊢ (u = w → (z ∈ u ↔ z ∈ w))
71	69, 70	sylan9bb 540	. . . . . . . . . . . 12 ⊢ ((v = z ⋀ u = w) → (v ∈ u ↔ z ∈ w))
72	71	adantl 388	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = z ⋀ ¬ ∀x x = w) ⋀ (v = z ⋀ u = w)) → (v ∈ u ↔ z ∈ w))
73		dveeq2 1212	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀x x = z → (v = z → ∀x v = z))
74		dveeq2 1212	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀x x = w → (u = w → ∀x u = w))
75	73, 74	im2anan9 563	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → ((v = z ⋀ u = w) → (∀x v = z ⋀ ∀x u = w)))
76	75	imp 350	. . . . . . . . . . . . 13 ⊢ (((¬ ∀x x = z ⋀ ¬ ∀x x = w) ⋀ (v = z ⋀ u = w)) → (∀x v = z ⋀ ∀x u = w))
77		19.26 1067	. . . . . . . . . . . . 13 ⊢ (∀x(v = z ⋀ u = w) ↔ (∀x v = z ⋀ ∀x u = w))
78	76, 77	sylibr 200	. . . . . . . . . . . 12 ⊢ (((¬ ∀x x = z ⋀ ¬ ∀x x = w) ⋀ (v = z ⋀ u = w)) → ∀x(v = z ⋀ u = w))
79		hba1 1003	. . . . . . . . . . . . 13 ⊢ (∀x(v = z ⋀ u = w) → ∀x∀x(v = z ⋀ u = w))
80	71	a4s 984	. . . . . . . . . . . . . 14 ⊢ (∀x(v = z ⋀ u = w) → (v ∈ u ↔ z ∈ w))
81	80	imbi2d 612	. . . . . . . . . . . . 13 ⊢ (∀x(v = z ⋀ u = w) → ((x = y → v ∈ u) ↔ (x = y → z ∈ w)))
82	79, 81	albid 1104	. . . . . . . . . . . 12 ⊢ (∀x(v = z ⋀ u = w) → (∀x(x = y → v ∈ u) ↔ ∀x(x = y → z ∈ w)))
83	78, 82	syl 10	. . . . . . . . . . 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 626	. . . . . . . . . 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 193	. . . . . . . . 9 ⊢ (((¬ ∀x x = z ⋀ ¬ ∀x x = w) ⋀ (v = z ⋀ u = w)) → (z ∈ w → ∀x(x = y → z ∈ w)))
86	85	exp32 377	. . . . . . . 8 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (v = z → (u = w → (z ∈ w → ∀x(x = y → z ∈ w)))))
87	86	19.23adv 1214	. . . . . . 7 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (∃v v = z → (u = w → (z ∈ w → ∀x(x = y → z ∈ w)))))
88	66, 87	mpi 44	. . . . . 6 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (u = w → (z ∈ w → ∀x(x = y → z ∈ w))))
89	88	19.23adv 1214	. . . . 5 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (∃u u = w → (z ∈ w → ∀x(x = y → z ∈ w))))
90	65, 89	mpi 44	. . . 4 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (z ∈ w → ∀x(x = y → z ∈ w)))
91	90	a1d 12	. . 3 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = w) → (x = y → (z ∈ w → ∀x(x = y → z ∈ w))))
92	91	a1d 12	. 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 758	1 ⊢ (¬ ∀x x = y → (x = y → (z ∈ w → ∀x(x = y → z ∈ w))))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 954   = wceq 956   ∈ wcel 958  ∃wex 980

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-15 1360

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981

Copyright terms: Public domain