Theorem axpowndlem2 4922

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

Proof of Theorem axpowndlem2

Step	Hyp	Ref	Expression
1		axpow 2733	. . . . . . 7 ⊢ ∃w∀y(∀w(w ∈ y → w ∈ z) → y ∈ w)
2		19.8a 1025	. . . . . . . . . . . 12 ⊢ (w ∈ y → ∃z w ∈ y)
3		ax-4 970	. . . . . . . . . . . 12 ⊢ (∀y w ∈ z → w ∈ z)
4	2, 3	imim12i 18	. . . . . . . . . . 11 ⊢ ((∃z w ∈ y → ∀y w ∈ z) → (w ∈ y → w ∈ z))
5	4	19.20i 989	. . . . . . . . . 10 ⊢ (∀w(∃z w ∈ y → ∀y w ∈ z) → ∀w(w ∈ y → w ∈ z))
6	5	imim1i 16	. . . . . . . . 9 ⊢ ((∀w(w ∈ y → w ∈ z) → y ∈ w) → (∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w))
7	6	19.20i 989	. . . . . . . 8 ⊢ (∀y(∀w(w ∈ y → w ∈ z) → y ∈ w) → ∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w))
8	7	19.22i 1036	. . . . . . 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 7	. . . . . 6 ⊢ ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w)
10	9	a1i 8	. . . . 5 ⊢ (¬ w = y → ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w))
11	10	ax-gen 960	. . . 4 ⊢ ∀w(¬ w = y → ∃w∀y(∀w(∃z w ∈ y → ∀y w ∈ z) → y ∈ w))
12		hbnae 1143	. . . . . 6 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
13		hbnae 1143	. . . . . 6 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
14	12, 13	hban 1006	. . . . 5 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀x(¬ ∀x x = y ⋀ ¬ ∀x x = z))
15		dveeq2 1208	. . . . . . . 8 ⊢ (¬ ∀x x = y → (w = y → ∀x w = y))
16	12, 15	hbnd 1105	. . . . . . 7 ⊢ (¬ ∀x x = y → (¬ w = y → ∀x ¬ w = y))
17	16	adantr 389	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (¬ w = y → ∀x ¬ w = y))
18		ax-17 968	. . . . . . 7 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀w(¬ ∀x x = y ⋀ ¬ ∀x x = z))
19		hbnae 1143	. . . . . . . . 9 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
20		hbnae 1143	. . . . . . . . 9 ⊢ (¬ ∀x x = z → ∀y ¬ ∀x x = z)
21	19, 20	hban 1006	. . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀y(¬ ∀x x = y ⋀ ¬ ∀x x = z))
22		hbnae 1143	. . . . . . . . . . 11 ⊢ (¬ ∀x x = y → ∀w ¬ ∀x x = y)
23		hbnae 1143	. . . . . . . . . . 11 ⊢ (¬ ∀x x = z → ∀w ¬ ∀x x = z)
24	22, 23	hban 1006	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀w(¬ ∀x x = y ⋀ ¬ ∀x x = z))
25		hbnae 1143	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
26		hbnae 1143	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
27	25, 26	hban 1006	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀z(¬ ∀x x = y ⋀ ¬ ∀x x = z))
28		dveel2 1350	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → (w ∈ y → ∀x w ∈ y))
29	28	adantr 389	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w ∈ y → ∀x w ∈ y))
30	27, 29	hbexd 1110	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∃z w ∈ y → ∀x∃z w ∈ y))
31		dveel2 1350	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = z → (w ∈ z → ∀x w ∈ z))
32	31	adantl 388	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w ∈ z → ∀x w ∈ z))
33	21, 32	hbald 1109	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∀y w ∈ z → ∀x∀y w ∈ z))
34	14, 30, 33	hbimd 1106	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ((∃z w ∈ y → ∀y w ∈ z) → ∀x(∃z w ∈ y → ∀y w ∈ z)))
35	24, 34	hbald 1109	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∀w(∃z w ∈ y → ∀y w ∈ z) → ∀x∀w(∃z w ∈ y → ∀y w ∈ z)))
36		dveel1 1349	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → (y ∈ w → ∀x y ∈ w))
37	36	adantr 389	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (y ∈ w → ∀x y ∈ w))
38	14, 35, 37	hbimd 1106	. . . . . . . 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 1109	. . . . . . 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 1110	. . . . . 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 1106	. . . . 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		equequ1 1130	. . . . . . . . 9 ⊢ (w = x → (w = y ↔ x = y))
43	42	negbid 609	. . . . . . . 8 ⊢ (w = x → (¬ w = y ↔ ¬ x = y))
44	43	adantl 388	. . . . . . 7 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ w = x) → (¬ w = y ↔ ¬ x = y))
45	18, 34	hbald 1109	. . . . . . . . . . 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 1106	. . . . . . . . . 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 1109	. . . . . . . . 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 4914	. . . . . . . . . . . . 13 ⊢ (¬ ∀x x = y → (w = x → ∀y w = x))
49	48	adantr 389	. . . . . . . . . . . 12 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w = x → ∀y w = x))
50	49	imdistani 443	. . . . . . . . . . 11 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ w = x) → ((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x))
51		hba1 1000	. . . . . . . . . . . . 13 ⊢ (∀y w = x → ∀y∀y w = x)
52	21, 51	hban 1006	. . . . . . . . . . . 12 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x) → ∀y((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x))
53		nd5 4914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ∀x x = z → (w = x → ∀z w = x))
54	53	imdistani 443	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ ∀x x = z ⋀ w = x) → (¬ ∀x x = z ⋀ ∀z w = x))
55		hba1 1000	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀z w = x → ∀z∀z w = x)
56		elequ1 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (w = x → (w ∈ y ↔ x ∈ y))
57	56	a4s 981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀z w = x → (w ∈ y ↔ x ∈ y))
58	55, 57	exbid 1101	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀z w = x → (∃z w ∈ y ↔ ∃z x ∈ y))
59	58	adantl 388	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ ∀x x = z ⋀ ∀z w = x) → (∃z w ∈ y ↔ ∃z x ∈ y))
60	54, 59	syl 10	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ ∀x x = z ⋀ w = x) → (∃z w ∈ y ↔ ∃z x ∈ y))
61	60	adantll 392	. . . . . . . . . . . . . . . . 17 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ w = x) → (∃z w ∈ y ↔ ∃z x ∈ y))
62	48	imdistani 443	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ ∀x x = y ⋀ w = x) → (¬ ∀x x = y ⋀ ∀y w = x))
63		elequ1 1132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (w = x → (w ∈ z ↔ x ∈ z))
64	63	a4s 981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀y w = x → (w ∈ z ↔ x ∈ z))
65	51, 64	albid 1100	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀y w = x → (∀y w ∈ z ↔ ∀y x ∈ z))
66	65	adantl 388	. . . . . . . . . . . . . . . . . . 19 ⊢ ((¬ ∀x x = y ⋀ ∀y w = x) → (∀y w ∈ z ↔ ∀y x ∈ z))
67	62, 66	syl 10	. . . . . . . . . . . . . . . . . 18 ⊢ ((¬ ∀x x = y ⋀ w = x) → (∀y w ∈ z ↔ ∀y x ∈ z))
68	67	adantlr 393	. . . . . . . . . . . . . . . . 17 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ w = x) → (∀y w ∈ z ↔ ∀y x ∈ z))
69	61, 68	imbi12d 624	. . . . . . . . . . . . . . . 16 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ w = x) → ((∃z w ∈ y → ∀y w ∈ z) ↔ (∃z x ∈ y → ∀y x ∈ z)))
70	69	ex 373	. . . . . . . . . . . . . . 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 1315	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∀w(∃z w ∈ y → ∀y w ∈ z) ↔ ∀x(∃z x ∈ y → ∀y x ∈ z)))
72	71	adantr 389	. . . . . . . . . . . . 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		elequ2 1133	. . . . . . . . . . . . . . 15 ⊢ (w = x → (y ∈ w ↔ y ∈ x))
74	73	a4s 981	. . . . . . . . . . . . . 14 ⊢ (∀y w = x → (y ∈ w ↔ y ∈ x))
75	74	adantl 388	. . . . . . . . . . . . 13 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x) → (y ∈ w ↔ y ∈ x))
76	72, 75	imbi12d 624	. . . . . . . . . . . 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	albid 1100	. . . . . . . . . . 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 10	. . . . . . . . . 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	ex 373	. . . . . . . . 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 1316	. . . . . . . 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 389	. . . . . . 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 624	. . . . . 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	ex 373	. . . . 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 1315	. . . 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 193	. . 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 1056	. 2 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x)))
87	86	ex 373	1 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (¬ x = y → ∃x∀y(∀x(∃z x ∈ y → ∀y x ∈ z) → y ∈ x))))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 951   = wceq 953   ∈ wcel 955  ∃wex 977

This theorem is referenced by:  axpowndlem3 4923

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-pow 2732

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain