Theorem axpowndlem2 3744

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

Assertion

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

Distinct variable group(s):   y,z

Proof of Theorem axpowndlem2

Step	Hyp	Ref	Expression
1		axpow 1082	. . . . . . 7 ⊢ ∃w∀y(∀w(w ∈ y → w ∈ z) → y ∈ w)
2		19.8a 712	. . . . . . . . . . . 12 ⊢ (w ∈ y → ∃z w ∈ y)
3		ax-4 673	. . . . . . . . . . . 12 ⊢ (∀y w ∈ z → w ∈ z)
4	2, 3	syl34 20	. . . . . . . . . . 11 ⊢ ((∃z w ∈ y → ∀y w ∈ z) → (w ∈ y → w ∈ z))
5	4	19.20i 691	. . . . . . . . . 10 ⊢ (∀w(∃z w ∈ y → ∀y w ∈ z) → ∀w(w ∈ y → w ∈ z))
6	5	syl4 19	. . . . . . . . 9 ⊢ ((∀w(w ∈ y → w ∈ z) → y ∈ w) → (∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w))
7	6	19.20i 691	. . . . . . . 8 ⊢ (∀y(∀w(w ∈ y → w ∈ z) → y ∈ w) → ∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w))
8	7	19.22i 723	. . . . . . 7 ⊢ (∃w∀y(∀w(w ∈ y → w ∈ z) → y ∈ w) → ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w))
9	1, 8	ax-mp 6	. . . . . 6 ⊢ ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)
10	9	a1i 7	. . . . 5 ⊢ (¬ w = y → ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w))
11	10	ax-gen 677	. . . 4 ⊢ ∀w(¬ w = y → ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w))
12		eq6 826	. . . . . 6 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
13		eq6 826	. . . . . 6 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
14	12, 13	hban 704	. . . . 5 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀x(¬ ∀x x = y ∧ ¬ ∀x x = z))
15		ddeeq2 1002	. . . . . . . 8 ⊢ (¬ ∀x x = y → (w = y → ∀x w = y))
16	12, 15	hbnd 786	. . . . . . 7 ⊢ (¬ ∀x x = y → (¬ w = y → ∀x ¬ w = y))
17	16	adantr 306	. . . . . 6 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (¬ w = y → ∀x ¬ w = y))
18		ax-17 925	. . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀w(¬ ∀x x = y ∧ ¬ ∀x x = z))
19		eq6 826	. . . . . . . . 9 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
20		eq6 826	. . . . . . . . 9 ⊢ (¬ ∀x x = z → ∀y ¬ ∀x x = z)
21	19, 20	hban 704	. . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀y(¬ ∀x x = y ∧ ¬ ∀x x = z))
22		eq6 826	. . . . . . . . . . 11 ⊢ (¬ ∀x x = y → ∀w ¬ ∀x x = y)
23		eq6 826	. . . . . . . . . . 11 ⊢ (¬ ∀x x = z → ∀w ¬ ∀x x = z)
24	22, 23	hban 704	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀w(¬ ∀x x = y ∧ ¬ ∀x x = z))
25		eq6 826	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
26		eq6 826	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
27	25, 26	hban 704	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀z(¬ ∀x x = y ∧ ¬ ∀x x = z))
28		ddeel2 1004	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → (w ∈ y → ∀x w ∈ y))
29	28	adantr 306	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w ∈ y → ∀x w ∈ y))
30	27, 29	hbexd 791	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∃z w ∈ y → ∀x∃z w ∈ y))
31		ddeel2 1004	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = z → (w ∈ z → ∀x w ∈ z))
32	31	adantl 305	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w ∈ z → ∀x w ∈ z))
33	21, 32	hbald 790	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∀y w ∈ z → ∀x∀y w ∈ z))
34	14, 30, 33	hbimd 787	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ((∃z w ∈ y → ∀y w ∈ z) → ∀x(∃z w ∈ y → ∀y w ∈ z)))
35	24, 34	hbald 790	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∀w(∃z w ∈ y → ∀y w ∈ z) → ∀x∀w(∃z w ∈ y → ∀y w ∈ z)))
36		ddeel1 1003	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → (y ∈ w → ∀x y ∈ w))
37	36	adantr 306	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (y ∈ w → ∀x y ∈ w))
38	14, 35, 37	hbimd 787	. . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ((∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) → ∀x(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)))
39	21, 38	hbald 790	. . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) → ∀x∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)))
40	18, 39	hbexd 791	. . . . . 6 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) → ∀x∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)))
41	14, 17, 40	hbimd 787	. . . . 5 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ((¬ w = y → ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)) → ∀x(¬ w = y → ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w))))
42		a8b 817	. . . . . . . . 9 ⊢ (w = x → (w = y ↔ x = y))
43	42	negbid 463	. . . . . . . 8 ⊢ (w = x → (¬ w = y ↔ ¬ x = y))
44	43	adantl 305	. . . . . . 7 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (¬ w = y ↔ ¬ x = y))
45	18, 34	hbald 790	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∀w(∃z w ∈ y → ∀y w ∈ z) → ∀x∀w(∃z w ∈ y → ∀y w ∈ z)))
46	14, 45, 37	hbimd 787	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ((∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) → ∀x(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)))
47	21, 46	hbald 790	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) → ∀x∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)))
48		nd5 3736	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → (w = x → ∀y w = x))
49	48	adantr 306	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w = x → ∀y w = x))
50	49	imdistani 340	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → ((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x))
51		hba1 698	. . . . . . . . . . . . 13 ⊢ (∀y w = x → ∀y∀y w = x)
52	21, 51	hban 704	. . . . . . . . . . . 12 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → ∀y((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x))
53		nd5 3736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ∀x x = z → (w = x → ∀z w = x))
54	53	imdistani 340	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ ∀x x = z ∧ w = x) → (¬ ∀x x = z ∧ ∀z w = x))
55		hba1 698	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀z w = x → ∀z∀z w = x)
56		a13b 819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (w = x → (w ∈ y ↔ x ∈ y))
57	56	a4s 682	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀z w = x → (w ∈ y ↔ x ∈ y))
58	55, 57	biexd 783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀z w = x → (∃z w ∈ y ↔ ∃z x ∈ y))
59	58	adantl 305	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ ∀x x = z ∧ ∀z w = x) → (∃z w ∈ y ↔ ∃z x ∈ y))
60	54, 59	syl 12	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ ∀x x = z ∧ w = x) → (∃z w ∈ y ↔ ∃z x ∈ y))
61	60	adantll 309	. . . . . . . . . . . . . . . . 17 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (∃z w ∈ y ↔ ∃z x ∈ y))
62	48	imdistani 340	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ ∀x x = y ∧ w = x) → (¬ ∀x x = y ∧ ∀y w = x))
63		a13b 819	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (w = x → (w ∈ z ↔ x ∈ z))
64	63	a4s 682	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀y w = x → (w ∈ z ↔ x ∈ z))
65	51, 64	biald 782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀y w = x → (∀y w ∈ z ↔ ∀y x ∈ z))
66	65	adantl 305	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ ∀x x = y ∧ ∀y w = x) → (∀y w ∈ z ↔ ∀y x ∈ z))
67	62, 66	syl 12	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ ∀x x = y ∧ w = x) → (∀y w ∈ z ↔ ∀y x ∈ z))
68	67	adantlr 310	. . . . . . . . . . . . . . . . 17 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (∀y w ∈ z ↔ ∀y x ∈ z))
69	61, 68	imbi12d 474	. . . . . . . . . . . . . . . 16 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → ((∃z w ∈ y → ∀y w ∈ z) ↔ (∃z x ∈ y → ∀y x ∈ z)))
70	69	exp 291	. . . . . . . . . . . . . . 15 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w = x → ((∃z w ∈ y → ∀y w ∈ z) ↔ (∃z x ∈ y → ∀y x ∈ z))))
71	14, 34, 70	cbvald 977	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∀w(∃z w ∈ y → ∀y w ∈ z) ↔ ∀x(∃z x ∈ y → ∀y x ∈ z)))
72	71	adantr 306	. . . . . . . . . . . . 13 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → (∀w(∃z w ∈ y → ∀y w ∈ z) ↔ ∀x(∃z x ∈ y → ∀y x ∈ z)))
73		a14b 820	. . . . . . . . . . . . . . 15 ⊢ (w = x → (y ∈ w ↔ y ∈ x))
74	73	a4s 682	. . . . . . . . . . . . . 14 ⊢ (∀y w = x → (y ∈ w ↔ y ∈ x))
75	74	adantl 305	. . . . . . . . . . . . 13 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → (y ∈ w ↔ y ∈ x))
76	72, 75	imbi12d 474	. . . . . . . . . . . 12 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → ((∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) ↔ (∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
77	52, 76	biald 782	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → (∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) ↔ ∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
78	50, 77	syl 12	. . . . . . . . . 10 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) ↔ ∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
79	78	exp 291	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w = x → (∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) ↔ ∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))))
80	14, 47, 79	cbvexd 978	. . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) ↔ ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
81	80	adantr 306	. . . . . . 7 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → (∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w) ↔ ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
82	44, 81	imbi12d 474	. . . . . 6 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → ((¬ w = y → ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)) ↔ (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))))
83	82	exp 291	. . . . 5 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w = x → ((¬ w = y → ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)) ↔ (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))))
84	14, 41, 83	cbvald 977	. . . 4 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∀w(¬ w = y → ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)) ↔ ∀x(¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))))
85	11, 84	mpbii 168	. . 3 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀x(¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
86	85	19.21bi 742	. 2 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
87	86	exp 291	1 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (¬ 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

This theorem is referenced by:  axpowndlem3 3745

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-17 925  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org