Theorem axpowndlem3 4971

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

Assertion

Ref	Expression
axpowndlem3	⊢ (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))

Distinct variable group:   y,z

Proof of Theorem axpowndlem3

Step	Hyp	Ref	Expression
1		axpowndlem2 4970	. 2 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))))
2		axpowndlem1 4969	. 2 ⊢ (∀x x = y → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
3		hbae 1149	. . . . . 6 ⊢ (∀x x = z → ∀x∀x x = z)
4		hbae 1149	. . . . . . 7 ⊢ (∀x x = z → ∀y∀x x = z)
5		nd3 4960	. . . . . . . . . . 11 ⊢ (∀x x = z → ¬ ∀y x ∈ z)
6		mtt 716	. . . . . . . . . . 11 ⊢ (¬ ∀y x ∈ z → (¬ ∃z x ∈ y ↔ (∃z x ∈ y → ∀y x ∈ z)))
7	5, 6	syl 10	. . . . . . . . . 10 ⊢ (∀x x = z → (¬ ∃z x ∈ y ↔ (∃z x ∈ y → ∀y x ∈ z)))
8		ax-10o 1144	. . . . . . . . . . . 12 ⊢ (∀z z = x → (∀z ¬ x ∈ y → ∀x ¬ x ∈ y))
9	8	alequcoms 1147	. . . . . . . . . . 11 ⊢ (∀x x = z → (∀z ¬ x ∈ y → ∀x ¬ x ∈ y))
10		alnex 1037	. . . . . . . . . . 11 ⊢ (∀z ¬ x ∈ y ↔ ¬ ∃z x ∈ y)
11		alnex 1037	. . . . . . . . . . 11 ⊢ (∀x ¬ x ∈ y ↔ ¬ ∃x x ∈ y)
12	9, 10, 11	3imtr3g 555	. . . . . . . . . 10 ⊢ (∀x x = z → (¬ ∃z x ∈ y → ¬ ∃x x ∈ y))
13	7, 12	sylbird 205	. . . . . . . . 9 ⊢ (∀x x = z → ((∃z x ∈ y → ∀y x ∈ z) → ¬ ∃x x ∈ y))
14	13	a4sd 989	. . . . . . . 8 ⊢ (∀x x = z → (∀x(∃z x ∈ y → ∀y x ∈ z) → ¬ ∃x x ∈ y))
15	14	imim1d 28	. . . . . . 7 ⊢ (∀x x = z → ((¬ ∃x x ∈ y → y ∈ x) → (∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
16	4, 15	19.20d 1000	. . . . . 6 ⊢ (∀x x = z → (∀y(¬ ∃x x ∈ y → y ∈ x) → ∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
17	3, 16	19.22d 1066	. . . . 5 ⊢ (∀x x = z → (∃x∀y(¬ ∃x x ∈ y → y ∈ x) → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
18		p0ex 2786	. . . . . . . . 9 ⊢ {∅} ∈ V
19		eleq2 1542	. . . . . . . . . . 11 ⊢ (x = {∅} → (w ∈ x ↔ w ∈ {∅}))
20	19	imbi2d 615	. . . . . . . . . 10 ⊢ (x = {∅} → ((w = ∅ → w ∈ x) ↔ (w = ∅ → w ∈ {∅})))
21	20	albidv 1282	. . . . . . . . 9 ⊢ (x = {∅} → (∀w(w = ∅ → w ∈ x) ↔ ∀w(w = ∅ → w ∈ {∅})))
22	18, 21	cla4ev 1876	. . . . . . . 8 ⊢ (∀w(w = ∅ → w ∈ {∅}) → ∃x∀w(w = ∅ → w ∈ x))
23		0ex 2726	. . . . . . . . . 10 ⊢ ∅ ∈ V
24	23	snid 2447	. . . . . . . . 9 ⊢ ∅ ∈ {∅}
25		eleq1 1541	. . . . . . . . 9 ⊢ (w = ∅ → (w ∈ {∅} ↔ ∅ ∈ {∅}))
26	24, 25	mpbiri 194	. . . . . . . 8 ⊢ (w = ∅ → w ∈ {∅})
27	22, 26	mpg 990	. . . . . . 7 ⊢ ∃x∀w(w = ∅ → w ∈ x)
28		n0 2301	. . . . . . . . . . 11 ⊢ (¬ w = ∅ ↔ ∃x x ∈ w)
29	28	con1bii 220	. . . . . . . . . 10 ⊢ (¬ ∃x x ∈ w ↔ w = ∅)
30	29	imbi1i 186	. . . . . . . . 9 ⊢ ((¬ ∃x x ∈ w → w ∈ x) ↔ (w = ∅ → w ∈ x))
31	30	albii 1003	. . . . . . . 8 ⊢ (∀w(¬ ∃x x ∈ w → w ∈ x) ↔ ∀w(w = ∅ → w ∈ x))
32	31	exbii 1055	. . . . . . 7 ⊢ (∃x∀w(¬ ∃x x ∈ w → w ∈ x) ↔ ∃x∀w(w = ∅ → w ∈ x))
33	27, 32	mpbir 190	. . . . . 6 ⊢ ∃x∀w(¬ ∃x x ∈ w → w ∈ x)
34		hbnae 1151	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
35		hbnae 1151	. . . . . . . 8 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
36		dveel1 1360	. . . . . . . . . . . 12 ⊢ (¬ ∀y y = x → (x ∈ w → ∀y x ∈ w))
37	36	nalequcoms 1148	. . . . . . . . . . 11 ⊢ (¬ ∀x x = y → (x ∈ w → ∀y x ∈ w))
38	34, 37	hbexd 1118	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → (∃x x ∈ w → ∀y∃x x ∈ w))
39	35, 38	hbnd 1113	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (¬ ∃x x ∈ w → ∀y ¬ ∃x x ∈ w))
40		dveel2 1361	. . . . . . . . . 10 ⊢ (¬ ∀y y = x → (w ∈ x → ∀y w ∈ x))
41	40	nalequcoms 1148	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (w ∈ x → ∀y w ∈ x))
42	35, 39, 41	hbimd 1114	. . . . . . . 8 ⊢ (¬ ∀x x = y → ((¬ ∃x x ∈ w → w ∈ x) → ∀y(¬ ∃x x ∈ w → w ∈ x)))
43		dveeq2 1216	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → (w = y → ∀x w = y))
44	43	imdistani 446	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ⋀ w = y) → (¬ ∀x x = y ⋀ ∀x w = y))
45		hba1 1007	. . . . . . . . . . . . . 14 ⊢ (∀x w = y → ∀x∀x w = y)
46		elequ2 1141	. . . . . . . . . . . . . . 15 ⊢ (w = y → (x ∈ w ↔ x ∈ y))
47	46	a4s 988	. . . . . . . . . . . . . 14 ⊢ (∀x w = y → (x ∈ w ↔ x ∈ y))
48	45, 47	exbid 1109	. . . . . . . . . . . . 13 ⊢ (∀x w = y → (∃x x ∈ w ↔ ∃x x ∈ y))
49	48	adantl 390	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ⋀ ∀x w = y) → (∃x x ∈ w ↔ ∃x x ∈ y))
50	44, 49	syl 10	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ⋀ w = y) → (∃x x ∈ w ↔ ∃x x ∈ y))
51	50	notbid 614	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ w = y) → (¬ ∃x x ∈ w ↔ ¬ ∃x x ∈ y))
52		elequ1 1140	. . . . . . . . . . 11 ⊢ (w = y → (w ∈ x ↔ y ∈ x))
53	52	adantl 390	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ w = y) → (w ∈ x ↔ y ∈ x))
54	51, 53	imbi12d 629	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ⋀ w = y) → ((¬ ∃x x ∈ w → w ∈ x) ↔ (¬ ∃x x ∈ y → y ∈ x)))
55	54	ex 373	. . . . . . . 8 ⊢ (¬ ∀x x = y → (w = y → ((¬ ∃x x ∈ w → w ∈ x) ↔ (¬ ∃x x ∈ y → y ∈ x))))
56	35, 42, 55	cbvald 1324	. . . . . . 7 ⊢ (¬ ∀x x = y → (∀w(¬ ∃x x ∈ w → w ∈ x) ↔ ∀y(¬ ∃x x ∈ y → y ∈ x)))
57	34, 56	exbid 1109	. . . . . 6 ⊢ (¬ ∀x x = y → (∃x∀w(¬ ∃x x ∈ w → w ∈ x) ↔ ∃x∀y(¬ ∃x x ∈ y → y ∈ x)))
58	33, 57	mpbii 193	. . . . 5 ⊢ (¬ ∀x x = y → ∃x∀y(¬ ∃x x ∈ y → y ∈ x))
59	17, 58	syl5 21	. . . 4 ⊢ (∀x x = z → (¬ ∀x x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
60	59	a1dd 42	. . 3 ⊢ (∀x x = z → (¬ ∀x x = y → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))))
61	60, 2	pm2.61d2 129	. 2 ⊢ (∀x x = z → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
62	1, 2, 61	pm2.61ii 130	1 ⊢ (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 958   = wceq 960   ∈ wcel 962  ∃wex 984  ∅c0 2291  {csn 2421

This theorem is referenced by:  axpowndlem4 4972

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-sep 2718  ax-nul 2725  ax-pow 2758  ax-reg 4608

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-ral 1656  df-rex 1657  df-v 1819  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-nul 2292  df-pw 2414  df-sn 2424  df-pr 2425

Copyright terms: Public domain