Theorem axpowndlem3 3745

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(s):   y,z

Proof of Theorem axpowndlem3

Step	Hyp	Ref	Expression
1		axpowndlem2 3744	. 2 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))))
2		axpowndlem1 3743	. 2 ⊢ (∀x x = y → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
3		nd3 3734	. . . . . . . . . . . . 13 ⊢ (∀x x = z → ¬ ∀y x ∈ z)
4		mtt 534	. . . . . . . . . . . . 13 ⊢ (¬ ∀y x ∈ z → (¬ ∃z x ∈ y ↔ (∃z x ∈ y → ∀y x ∈ z)))
5	3, 4	syl 12	. . . . . . . . . . . 12 ⊢ (∀x x = z → (¬ ∃z x ∈ y ↔ (∃z x ∈ y → ∀y x ∈ z)))
6		ax-10 800	. . . . . . . . . . . . . 14 ⊢ (∀z z = x → (∀z ¬ x ∈ y → ∀x ¬ x ∈ y))
7	6	eq4s 822	. . . . . . . . . . . . 13 ⊢ (∀x x = z → (∀z ¬ x ∈ y → ∀x ¬ x ∈ y))
8		alnex 716	. . . . . . . . . . . . 13 ⊢ (∀z ¬ x ∈ y ↔ ¬ ∃z x ∈ y)
9		alnex 716	. . . . . . . . . . . . 13 ⊢ (∀x ¬ x ∈ y ↔ ¬ ∃x x ∈ y)
10	7, 8, 9	3imtr3g 425	. . . . . . . . . . . 12 ⊢ (∀x x = z → (¬ ∃z x ∈ y → ¬ ∃x x ∈ y))
11	5, 10	sylbird 180	. . . . . . . . . . 11 ⊢ (∀x x = z → ((∃z x ∈ y → ∀y x ∈ z) → ¬ ∃x x ∈ y))
12	11	a4sd 683	. . . . . . . . . 10 ⊢ (∀x x = z → (∀x(∃z x ∈ y → ∀y x ∈ z) → ¬ ∃x x ∈ y))
13	12	syl4d 28	. . . . . . . . 9 ⊢ (∀x x = z → ((¬ ∃x x ∈ y → y ∈ x) → (∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
14	13	del36 838	. . . . . . . 8 ⊢ (∀x x = z → (∀y(¬ ∃x x ∈ y → y ∈ x) → ∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
15	14	del42 841	. . . . . . 7 ⊢ (∀x x = z → (∃x∀y(¬ ∃x x ∈ y → y ∈ x) → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
16		p0ex 1885	. . . . . . . . . . 11 ⊢ {∅} ∈ V
17		eleq2 1150	. . . . . . . . . . . . 13 ⊢ (x = {∅} → (w ∈ x ↔ w ∈ {∅}))
18	17	imbi2d 464	. . . . . . . . . . . 12 ⊢ (x = {∅} → ((w = ∅ → w ∈ x) ↔ (w = ∅ → w ∈ {∅})))
19	18	bialdv 935	. . . . . . . . . . 11 ⊢ (x = {∅} → (∀w(w = ∅ → w ∈ x) ↔ ∀w(w = ∅ → w ∈ {∅})))
20	16, 19	cla4ev 1401	. . . . . . . . . 10 ⊢ (∀w(w = ∅ → w ∈ {∅}) → ∃x∀w(w = ∅ → w ∈ x))
21		0ex 1745	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
22	21	snid 1830	. . . . . . . . . . 11 ⊢ ∅ ∈ {∅}
23		eleq1 1149	. . . . . . . . . . 11 ⊢ (w = ∅ → (w ∈ {∅} ↔ ∅ ∈ {∅}))
24	22, 23	mpbiri 169	. . . . . . . . . 10 ⊢ (w = ∅ → w ∈ {∅})
25	20, 24	mpg 684	. . . . . . . . 9 ⊢ ∃x∀w(w = ∅ → w ∈ x)
26		n0 1714	. . . . . . . . . . . . 13 ⊢ (¬ w = ∅ ↔ ∃x x ∈ w)
27	26	bicon1i 193	. . . . . . . . . . . 12 ⊢ (¬ ∃x x ∈ w ↔ w = ∅)
28	27	imbi1i 161	. . . . . . . . . . 11 ⊢ ((¬ ∃x x ∈ w → w ∈ x) ↔ (w = ∅ → w ∈ x))
29	28	bial 695	. . . . . . . . . 10 ⊢ (∀w(¬ ∃x x ∈ w → w ∈ x) ↔ ∀w(w = ∅ → w ∈ x))
30	29	biex 733	. . . . . . . . 9 ⊢ (∃x∀w(¬ ∃x x ∈ w → w ∈ x) ↔ ∃x∀w(w = ∅ → w ∈ x))
31	25, 30	mpbir 165	. . . . . . . 8 ⊢ ∃x∀w(¬ ∃x x ∈ w → w ∈ x)
32		eq6 826	. . . . . . . . 9 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
33		eq6 826	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
34		ddeel1 1003	. . . . . . . . . . . . . 14 ⊢ (¬ ∀y y = x → (x ∈ w → ∀y x ∈ w))
35	34	eq4ds 823	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → (x ∈ w → ∀y x ∈ w))
36	32, 35	hbexd 791	. . . . . . . . . . . 12 ⊢ (¬ ∀x x = y → (∃x x ∈ w → ∀y∃x x ∈ w))
37	33, 36	hbnd 786	. . . . . . . . . . 11 ⊢ (¬ ∀x x = y → (¬ ∃x x ∈ w → ∀y ¬ ∃x x ∈ w))
38		ddeel2 1004	. . . . . . . . . . . 12 ⊢ (¬ ∀y y = x → (w ∈ x → ∀y w ∈ x))
39	38	eq4ds 823	. . . . . . . . . . 11 ⊢ (¬ ∀x x = y → (w ∈ x → ∀y w ∈ x))
40	33, 37, 39	hbimd 787	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → ((¬ ∃x x ∈ w → w ∈ x) → ∀y(¬ ∃x x ∈ w → w ∈ x)))
41		ddeeq2 1002	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀x x = y → (w = y → ∀x w = y))
42	41	imdistani 340	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = y ∧ w = y) → (¬ ∀x x = y ∧ ∀x w = y))
43		hba1 698	. . . . . . . . . . . . . . . 16 ⊢ (∀x w = y → ∀x∀x w = y)
44		a14b 820	. . . . . . . . . . . . . . . . 17 ⊢ (w = y → (x ∈ w ↔ x ∈ y))
45	44	a4s 682	. . . . . . . . . . . . . . . 16 ⊢ (∀x w = y → (x ∈ w ↔ x ∈ y))
46	43, 45	biexd 783	. . . . . . . . . . . . . . 15 ⊢ (∀x w = y → (∃x x ∈ w ↔ ∃x x ∈ y))
47	46	adantl 305	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = y ∧ ∀x w = y) → (∃x x ∈ w ↔ ∃x x ∈ y))
48	42, 47	syl 12	. . . . . . . . . . . . 13 ⊢ ((¬ ∀x x = y ∧ w = y) → (∃x x ∈ w ↔ ∃x x ∈ y))
49	48	negbid 463	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ∧ w = y) → (¬ ∃x x ∈ w ↔ ¬ ∃x x ∈ y))
50		a13b 819	. . . . . . . . . . . . 13 ⊢ (w = y → (w ∈ x ↔ y ∈ x))
51	50	adantl 305	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ∧ w = y) → (w ∈ x ↔ y ∈ x))
52	49, 51	imbi12d 474	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ∧ w = y) → ((¬ ∃x x ∈ w → w ∈ x) ↔ (¬ ∃x x ∈ y → y ∈ x)))
53	52	exp 291	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → (w = y → ((¬ ∃x x ∈ w → w ∈ x) ↔ (¬ ∃x x ∈ y → y ∈ x))))
54	33, 40, 53	cbvald 977	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (∀w(¬ ∃x x ∈ w → w ∈ x) ↔ ∀y(¬ ∃x x ∈ y → y ∈ x)))
55	32, 54	biexd 783	. . . . . . . 8 ⊢ (¬ ∀x x = y → (∃x∀w(¬ ∃x x ∈ w → w ∈ x) ↔ ∃x∀y(¬ ∃x x ∈ y → y ∈ x)))
56	31, 55	mpbii 168	. . . . . . 7 ⊢ (¬ ∀x x = y → ∃x∀y(¬ ∃x x ∈ y → y ∈ x))
57	15, 56	syl5 22	. . . . . 6 ⊢ (∀x x = z → (¬ ∀x x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
58	57	imp 277	. . . . 5 ⊢ ((∀x x = z ∧ ¬ ∀x x = y) → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))
59	58	a1d 14	. . . 4 ⊢ ((∀x x = z ∧ ¬ ∀x x = y) → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
60	59	exp 291	. . 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 111	. 2 ⊢ (∀x x = z → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
62	1, 2, 61	pm2.61ii 113	1 ⊢ (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∅c0 1707  {csn 1808

This theorem is referenced by:  axpowndlem4 3746

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077  ax-reg 1078

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812

metamath.org