Theorem axunnd 4931

Description: A version of the Axiom of Union with no distinct variable conditions.

Assertion

Ref	Expression
axunnd	⊢ ∃x∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x)

Proof of Theorem axunnd

Step	Hyp	Ref	Expression
1		axunndlem1 4930	. . . 4 ⊢ ∃w∀y(∃w(y ∈ w ⋀ w ∈ z) → y ∈ w)
2		hbnae 1146	. . . . . 6 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
3		hbnae 1146	. . . . . 6 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
4	2, 3	hban 1008	. . . . 5 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀x(¬ ∀x x = y ⋀ ¬ ∀x x = z))
5		hbnae 1146	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
6		hbnae 1146	. . . . . . 7 ⊢ (¬ ∀x x = z → ∀y ¬ ∀x x = z)
7	5, 6	hban 1008	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀y(¬ ∀x x = y ⋀ ¬ ∀x x = z))
8		ax-17 970	. . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∀w(¬ ∀x x = y ⋀ ¬ ∀x x = z))
9		dveel1 1355	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → (y ∈ w → ∀x y ∈ w))
10	9	adantr 389	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (y ∈ w → ∀x y ∈ w))
11		dveel2 1356	. . . . . . . . . 10 ⊢ (¬ ∀x x = z → (w ∈ z → ∀x w ∈ z))
12	11	adantl 388	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w ∈ z → ∀x w ∈ z))
13	10, 12	hband 1110	. . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ((y ∈ w ⋀ w ∈ z) → ∀x(y ∈ w ⋀ w ∈ z)))
14	8, 13	hbexd 1113	. . . . . . 7 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∃w(y ∈ w ⋀ w ∈ z) → ∀x∃w(y ∈ w ⋀ w ∈ z)))
15	4, 14, 10	hbimd 1109	. . . . . 6 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ((∃w(y ∈ w ⋀ w ∈ z) → y ∈ w) → ∀x(∃w(y ∈ w ⋀ w ∈ z) → y ∈ w)))
16	7, 15	hbald 1112	. . . . 5 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∀y(∃w(y ∈ w ⋀ w ∈ z) → y ∈ w) → ∀x∀y(∃w(y ∈ w ⋀ w ∈ z) → y ∈ w)))
17		nd5 4925	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (w = x → ∀y w = x))
18	17	adantr 389	. . . . . . . 8 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w = x → ∀y w = x))
19	18	imdistani 443	. . . . . . 7 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ w = x) → ((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x))
20		hba1 1002	. . . . . . . . 9 ⊢ (∀y w = x → ∀y∀y w = x)
21	7, 20	hban 1008	. . . . . . . 8 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x) → ∀y((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x))
22		elequ2 1136	. . . . . . . . . . . . 13 ⊢ (w = x → (y ∈ w ↔ y ∈ x))
23		elequ1 1135	. . . . . . . . . . . . 13 ⊢ (w = x → (w ∈ z ↔ x ∈ z))
24	22, 23	anbi12d 627	. . . . . . . . . . . 12 ⊢ (w = x → ((y ∈ w ⋀ w ∈ z) ↔ (y ∈ x ⋀ x ∈ z)))
25	24	a1i 8	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w = x → ((y ∈ w ⋀ w ∈ z) ↔ (y ∈ x ⋀ x ∈ z))))
26	4, 13, 25	cbvexd 1320	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∃w(y ∈ w ⋀ w ∈ z) ↔ ∃x(y ∈ x ⋀ x ∈ z)))
27	26	adantr 389	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x) → (∃w(y ∈ w ⋀ w ∈ z) ↔ ∃x(y ∈ x ⋀ x ∈ z)))
28	22	a4s 983	. . . . . . . . . 10 ⊢ (∀y w = x → (y ∈ w ↔ y ∈ x))
29	28	adantl 388	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x) → (y ∈ w ↔ y ∈ x))
30	27, 29	imbi12d 625	. . . . . . . 8 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x) → ((∃w(y ∈ w ⋀ w ∈ z) → y ∈ w) ↔ (∃x(y ∈ x ⋀ x ∈ z) → y ∈ x)))
31	21, 30	albid 1103	. . . . . . 7 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ ∀y w = x) → (∀y(∃w(y ∈ w ⋀ w ∈ z) → y ∈ w) ↔ ∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x)))
32	19, 31	syl 10	. . . . . 6 ⊢ (((¬ ∀x x = y ⋀ ¬ ∀x x = z) ⋀ w = x) → (∀y(∃w(y ∈ w ⋀ w ∈ z) → y ∈ w) ↔ ∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x)))
33	32	ex 373	. . . . 5 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (w = x → (∀y(∃w(y ∈ w ⋀ w ∈ z) → y ∈ w) ↔ ∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x))))
34	4, 16, 33	cbvexd 1320	. . . 4 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → (∃w∀y(∃w(y ∈ w ⋀ w ∈ z) → y ∈ w) ↔ ∃x∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x)))
35	1, 34	mpbii 193	. . 3 ⊢ ((¬ ∀x x = y ⋀ ¬ ∀x x = z) → ∃x∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x))
36	35	ex 373	. 2 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → ∃x∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x)))
37		hbae 1144	. . . 4 ⊢ (∀x x = y → ∀y∀x x = y)
38		hbae 1144	. . . . . 6 ⊢ (∀x x = y → ∀x∀x x = y)
39		elirrv 4581	. . . . . . . 8 ⊢ ¬ y ∈ y
40		elequ2 1136	. . . . . . . . 9 ⊢ (x = y → (y ∈ x ↔ y ∈ y))
41		pm3.26 319	. . . . . . . . 9 ⊢ ((y ∈ x ⋀ x ∈ z) → y ∈ x)
42	40, 41	syl5bi 208	. . . . . . . 8 ⊢ (x = y → ((y ∈ x ⋀ x ∈ z) → y ∈ y))
43	39, 42	mtoi 107	. . . . . . 7 ⊢ (x = y → ¬ (y ∈ x ⋀ x ∈ z))
44	43	a4s 983	. . . . . 6 ⊢ (∀x x = y → ¬ (y ∈ x ⋀ x ∈ z))
45	38, 44	nexd 1101	. . . . 5 ⊢ (∀x x = y → ¬ ∃x(y ∈ x ⋀ x ∈ z))
46	45	pm2.21d 78	. . . 4 ⊢ (∀x x = y → (∃x(y ∈ x ⋀ x ∈ z) → y ∈ x))
47	37, 46	19.21ai 997	. . 3 ⊢ (∀x x = y → ∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x))
48		19.8a 1028	. . 3 ⊢ (∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x) → ∃x∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x))
49	47, 48	syl 10	. 2 ⊢ (∀x x = y → ∃x∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x))
50		hbae 1144	. . . 4 ⊢ (∀x x = z → ∀y∀x x = z)
51		hbae 1144	. . . . . 6 ⊢ (∀x x = z → ∀x∀x x = z)
52		elirrv 4581	. . . . . . . 8 ⊢ ¬ z ∈ z
53		elequ1 1135	. . . . . . . . 9 ⊢ (x = z → (x ∈ z ↔ z ∈ z))
54		pm3.27 323	. . . . . . . . 9 ⊢ ((y ∈ x ⋀ x ∈ z) → x ∈ z)
55	53, 54	syl5bi 208	. . . . . . . 8 ⊢ (x = z → ((y ∈ x ⋀ x ∈ z) → z ∈ z))
56	52, 55	mtoi 107	. . . . . . 7 ⊢ (x = z → ¬ (y ∈ x ⋀ x ∈ z))
57	56	a4s 983	. . . . . 6 ⊢ (∀x x = z → ¬ (y ∈ x ⋀ x ∈ z))
58	51, 57	nexd 1101	. . . . 5 ⊢ (∀x x = z → ¬ ∃x(y ∈ x ⋀ x ∈ z))
59	58	pm2.21d 78	. . . 4 ⊢ (∀x x = z → (∃x(y ∈ x ⋀ x ∈ z) → y ∈ x))
60	50, 59	19.21ai 997	. . 3 ⊢ (∀x x = z → ∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x))
61	60, 48	syl 10	. 2 ⊢ (∀x x = z → ∃x∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x))
62	36, 49, 61	pm2.61ii 130	1 ⊢ ∃x∀y(∃x(y ∈ x ⋀ x ∈ z) → y ∈ x)

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

This theorem is referenced by:  zfcndun 4950

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-pow 2738  ax-pr 2775  ax-un 2862  ax-reg 4576

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  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  df-op 2413  df-br 2616  df-opab 2663  df-eprel 2828  df-fr 2913

Copyright terms: Public domain