Theorem axpowndlem3 4934

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 4933	. 2 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))))
2		axpowndlem1 4932	. 2 ⊢ (∀x x = y → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
3		hbae 1144	. . . . . 6 ⊢ (∀x x = z → ∀x∀x x = z)
4		hbae 1144	. . . . . . 7 ⊢ (∀x x = z → ∀y∀x x = z)
5		nd3 4923	. . . . . . . . . . 11 ⊢ (∀x x = z → ¬ ∀y x ∈ z)
6		mtt 711	. . . . . . . . . . 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 1139	. . . . . . . . . . . 12 ⊢ (∀z z = x → (∀z ¬ x ∈ y → ∀x ¬ x ∈ y))
9	8	alequcoms 1142	. . . . . . . . . . 11 ⊢ (∀x x = z → (∀z ¬ x ∈ y → ∀x ¬ x ∈ y))
10		alnex 1032	. . . . . . . . . . 11 ⊢ (∀z ¬ x ∈ y ↔ ¬ ∃z x ∈ y)
11		alnex 1032	. . . . . . . . . . 11 ⊢ (∀x ¬ x ∈ y ↔ ¬ ∃x x ∈ y)
12	9, 10, 11	3imtr3g 551	. . . . . . . . . 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 984	. . . . . . . 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 995	. . . . . 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 1061	. . . . 5 ⊢ (∀x x = z → (∃x∀y(¬ ∃x x ∈ y → y ∈ x) → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
18		p0ex 2766	. . . . . . . . 9 ⊢ {∅} ∈ V
19		eleq2 1533	. . . . . . . . . . 11 ⊢ (x = {∅} → (w ∈ x ↔ w ∈ {∅}))
20	19	imbi2d 611	. . . . . . . . . 10 ⊢ (x = {∅} → ((w = ∅ → w ∈ x) ↔ (w = ∅ → w ∈ {∅})))
21	20	albidv 1277	. . . . . . . . 9 ⊢ (x = {∅} → (∀w(w = ∅ → w ∈ x) ↔ ∀w(w = ∅ → w ∈ {∅})))
22	18, 21	cla4ev 1866	. . . . . . . 8 ⊢ (∀w(w = ∅ → w ∈ {∅}) → ∃x∀w(w = ∅ → w ∈ x))
23		0ex 2707	. . . . . . . . . 10 ⊢ ∅ ∈ V
24	23	snid 2432	. . . . . . . . 9 ⊢ ∅ ∈ {∅}
25		eleq1 1532	. . . . . . . . 9 ⊢ (w = ∅ → (w ∈ {∅} ↔ ∅ ∈ {∅}))
26	24, 25	mpbiri 194	. . . . . . . 8 ⊢ (w = ∅ → w ∈ {∅})
27	22, 26	mpg 985	. . . . . . 7 ⊢ ∃x∀w(w = ∅ → w ∈ x)
28		n0 2286	. . . . . . . . . . 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 998	. . . . . . . 8 ⊢ (∀w(¬ ∃x x ∈ w → w ∈ x) ↔ ∀w(w = ∅ → w ∈ x))
32	31	exbii 1050	. . . . . . 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 1146	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
35		hbnae 1146	. . . . . . . 8 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
36		dveel1 1355	. . . . . . . . . . . 12 ⊢ (¬ ∀y y = x → (x ∈ w → ∀y x ∈ w))
37	36	nalequcoms 1143	. . . . . . . . . . 11 ⊢ (¬ ∀x x = y → (x ∈ w → ∀y x ∈ w))
38	34, 37	hbexd 1113	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → (∃x x ∈ w → ∀y∃x x ∈ w))
39	35, 38	hbnd 1108	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (¬ ∃x x ∈ w → ∀y ¬ ∃x x ∈ w))
40		dveel2 1356	. . . . . . . . . 10 ⊢ (¬ ∀y y = x → (w ∈ x → ∀y w ∈ x))
41	40	nalequcoms 1143	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (w ∈ x → ∀y w ∈ x))
42	35, 39, 41	hbimd 1109	. . . . . . . 8 ⊢ (¬ ∀x x = y → ((¬ ∃x x ∈ w → w ∈ x) → ∀y(¬ ∃x x ∈ w → w ∈ x)))
43		dveeq2 1211	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → (w = y → ∀x w = y))
44	43	imdistani 443	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ⋀ w = y) → (¬ ∀x x = y ⋀ ∀x w = y))
45		hba1 1002	. . . . . . . . . . . . . 14 ⊢ (∀x w = y → ∀x∀x w = y)
46		elequ2 1136	. . . . . . . . . . . . . . 15 ⊢ (w = y → (x ∈ w ↔ x ∈ y))
47	46	a4s 983	. . . . . . . . . . . . . 14 ⊢ (∀x w = y → (x ∈ w ↔ x ∈ y))
48	45, 47	exbid 1104	. . . . . . . . . . . . 13 ⊢ (∀x w = y → (∃x x ∈ w ↔ ∃x x ∈ y))
49	48	adantl 388	. . . . . . . . . . . 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	negbid 610	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ w = y) → (¬ ∃x x ∈ w ↔ ¬ ∃x x ∈ y))
52		elequ1 1135	. . . . . . . . . . 11 ⊢ (w = y → (w ∈ x ↔ y ∈ x))
53	52	adantl 388	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ w = y) → (w ∈ x ↔ y ∈ x))
54	51, 53	imbi12d 625	. . . . . . . . 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 1319	. . . . . . 7 ⊢ (¬ ∀x x = y → (∀w(¬ ∃x x ∈ w → w ∈ x) ↔ ∀y(¬ ∃x x ∈ y → y ∈ x)))
57	34, 56	exbid 1104	. . . . . 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 953   = wceq 955   ∈ wcel 957  ∃wex 979  ∅c0 2277  {csn 2406

This theorem is referenced by:  axpowndlem4 4935

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-reg 4576

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410

Copyright terms: Public domain