Theorem axregndlem2 4935

Description: Lemma for the Axiom of Regularity with no distinct variable conditions.

Assertion

Ref	Expression
axregndlem2	⊢ (x ∈ y → ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y)))

Distinct variable group:   y,z

Proof of Theorem axregndlem2

Step	Hyp	Ref	Expression
1		axreg 4574	. . . . . 6 ⊢ (w ∈ y → ∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y)))
2	1	ax-gen 961	. . . . 5 ⊢ ∀w(w ∈ y → ∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y)))
3		hbnae 1145	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
4		hbnae 1145	. . . . . . 7 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
5	3, 4	hban 1007	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀x(¬ ∀x x = y ⋀ ¬ ∀x x = z))
6		dveel2 1355	. . . . . . . 8 ⊢ (¬ ∀x x = y → (w ∈ y → ∀x w ∈ y))
7	6	adantr 389	. . . . . . 7 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w ∈ y → ∀x w ∈ y))
8		ax-17 969	. . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀w(¬ ∀x x = y ⋀ ¬ ∀x x = z))
9		hbnae 1145	. . . . . . . . . . 11 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
10		hbnae 1145	. . . . . . . . . . 11 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
11	9, 10	hban 1007	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀z(¬ ∀x x = y ⋀ ¬ ∀x x = z))
12		dveel1 1354	. . . . . . . . . . . 12 ⊢ (¬ ∀x x = z → (z ∈ w → ∀x z ∈ w))
13	12	adantl 388	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (z ∈ w → ∀x z ∈ w))
14		ax-15 1358	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (z ∈ y → ∀x z ∈ y)))
15	14	impcom 351	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (z ∈ y → ∀x z ∈ y))
16	5, 15	hbnd 1107	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (¬ z ∈ y → ∀x ¬ z ∈ y))
17	5, 13, 16	hbimd 1108	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ((z ∈ w → ¬ z ∈ y) → ∀x(z ∈ w → ¬ z ∈ y)))
18	11, 17	hbald 1111	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∀z(z ∈ w → ¬ z ∈ y) → ∀x∀z(z ∈ w → ¬ z ∈ y)))
19	7, 18	hband 1109	. . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ((w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y)) → ∀x(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y))))
20	8, 19	hbexd 1112	. . . . . . 7 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y)) → ∀x∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y))))
21	5, 7, 20	hbimd 1108	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ((w ∈ y → ∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y))) → ∀x(w ∈ y → ∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y)))))
22		elequ1 1134	. . . . . . . . 9 ⊢ (w = x → (w ∈ y ↔ x ∈ y))
23	22	adantl 388	. . . . . . . 8 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ w = x) → (w ∈ y ↔ x ∈ y))
24	22	adantl 388	. . . . . . . . . . . . 13 ⊢ ((¬ ∀x x = z ⋀ w = x) → (w ∈ y ↔ x ∈ y))
25		nd5 4922	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀x x = z → (w = x → ∀z w = x))
26	25	imdistani 443	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = z ⋀ w = x) → (¬ ∀x x = z ⋀ ∀z w = x))
27		hba1 1001	. . . . . . . . . . . . . . . 16 ⊢ (∀z w = x → ∀z∀z w = x)
28	10, 27	hban 1007	. . . . . . . . . . . . . . 15 ⊢ ((¬ ∀x x = z ⋀ ∀z w = x) → ∀z(¬ ∀x x = z ⋀ ∀z w = x))
29		elequ2 1135	. . . . . . . . . . . . . . . . . 18 ⊢ (w = x → (z ∈ w ↔ z ∈ x))
30	29	imbi1d 612	. . . . . . . . . . . . . . . . 17 ⊢ (w = x → ((z ∈ w → ¬ z ∈ y) ↔ (z ∈ x → ¬ z ∈ y)))
31	30	a4s 982	. . . . . . . . . . . . . . . 16 ⊢ (∀z w = x → ((z ∈ w → ¬ z ∈ y) ↔ (z ∈ x → ¬ z ∈ y)))
32	31	adantl 388	. . . . . . . . . . . . . . 15 ⊢ ((¬ ∀x x = z ⋀ ∀z w = x) → ((z ∈ w → ¬ z ∈ y) ↔ (z ∈ x → ¬ z ∈ y)))
33	28, 32	albid 1102	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = z ⋀ ∀z w = x) → (∀z(z ∈ w → ¬ z ∈ y) ↔ ∀z(z ∈ x → ¬ z ∈ y)))
34	26, 33	syl 10	. . . . . . . . . . . . 13 ⊢ ((¬ ∀x x = z ⋀ w = x) → (∀z(z ∈ w → ¬ z ∈ y) ↔ ∀z(z ∈ x → ¬ z ∈ y)))
35	24, 34	anbi12d 627	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = z ⋀ w = x) → ((w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y)) ↔ (x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y))))
36	35	ex 373	. . . . . . . . . . 11 ⊢ (¬ ∀x x = z → (w = x → ((w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y)) ↔ (x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y)))))
37	36	adantl 388	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w = x → ((w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y)) ↔ (x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y)))))
38	5, 19, 37	cbvexd 1319	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y)) ↔ ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y))))
39	38	adantr 389	. . . . . . . 8 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ w = x) → (∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y)) ↔ ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y))))
40	23, 39	imbi12d 625	. . . . . . 7 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ w = x) → ((w ∈ y → ∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y))) ↔ (x ∈ y → ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y)))))
41	40	ex 373	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w = x → ((w ∈ y → ∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y))) ↔ (x ∈ y → ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y))))))
42	5, 21, 41	cbvald 1318	. . . . 5 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∀w(w ∈ y → ∃w(w ∈ y ⋀ ∀z(z ∈ w → ¬ z ∈ y))) ↔ ∀x(x ∈ y → ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y)))))
43	2, 42	mpbii 193	. . . 4 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀x(x ∈ y → ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y))))
44	43	19.21bi 1058	. . 3 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (x ∈ y → ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y))))
45	44	ex 373	. 2 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (x ∈ y → ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y)))))
46		elirrv 4578	. . . . 5 ⊢ ¬ x ∈ x
47		elequ2 1135	. . . . 5 ⊢ (x = y → (x ∈ x ↔ x ∈ y))
48	46, 47	mtbii 715	. . . 4 ⊢ (x = y → ¬ x ∈ y)
49	48	a4s 982	. . 3 ⊢ (∀x x = y → ¬ x ∈ y)
50	49	pm2.21d 78	. 2 ⊢ (∀x x = y → (x ∈ y → ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y))))
51		axregndlem1 4934	. 2 ⊢ (∀x x = z → (x ∈ y → ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y))))
52	45, 50, 51	pm2.61ii 130	1 ⊢ (x ∈ y → ∃x(x ∈ y ⋀ ∀z(z ∈ x → ¬ z ∈ y)))

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

This theorem is referenced by:  axregnd 4936

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-15 1358  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-reg 4573

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409

Copyright terms: Public domain