Theorem axunnd 3742

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 3741	. . . 4 ⊢ ∃w∀y(∃w(y ∈ w ∧ w ∈ z) → y ∈ w)
2		eq6 826	. . . . . 6 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
3		eq6 826	. . . . . 6 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
4	2, 3	hban 704	. . . . 5 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀x(¬ ∀x x = y ∧ ¬ ∀x x = z))
5		eq6 826	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
6		eq6 826	. . . . . . 7 ⊢ (¬ ∀x x = z → ∀y ¬ ∀x x = z)
7	5, 6	hban 704	. . . . . 6 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀y(¬ ∀x x = y ∧ ¬ ∀x x = z))
8		ax-17 925	. . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∀w(¬ ∀x x = y ∧ ¬ ∀x x = z))
9		ddeel1 1003	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → (y ∈ w → ∀x y ∈ w))
10	9	adantr 306	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (y ∈ w → ∀x y ∈ w))
11		ddeel2 1004	. . . . . . . . . 10 ⊢ (¬ ∀x x = z → (w ∈ z → ∀x w ∈ z))
12	11	adantl 305	. . . . . . . . 9 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w ∈ z → ∀x w ∈ z))
13	10, 12	hband 788	. . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ((y ∈ w ∧ w ∈ z) → ∀x(y ∈ w ∧ w ∈ z)))
14	8, 13	hbexd 791	. . . . . . 7 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∃w(y ∈ w ∧ w ∈ z) → ∀x∃w(y ∈ w ∧ w ∈ z)))
15	4, 14, 10	hbimd 787	. . . . . 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 790	. . . . 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 3736	. . . . . . . . 9 ⊢ (¬ ∀x x = y → (w = x → ∀y w = x))
18	17	adantr 306	. . . . . . . 8 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w = x → ∀y w = x))
19	18	imdistani 340	. . . . . . 7 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ w = x) → ((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x))
20		hba1 698	. . . . . . . . 9 ⊢ (∀y w = x → ∀y∀y w = x)
21	7, 20	hban 704	. . . . . . . 8 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → ∀y((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x))
22		a14b 820	. . . . . . . . . . . . 13 ⊢ (w = x → (y ∈ w ↔ y ∈ x))
23		a13b 819	. . . . . . . . . . . . 13 ⊢ (w = x → (w ∈ z ↔ x ∈ z))
24	22, 23	anbi12d 476	. . . . . . . . . . . 12 ⊢ (w = x → ((y ∈ w ∧ w ∈ z) ↔ (y ∈ x ∧ x ∈ z)))
25	24	a1i 7	. . . . . . . . . . 11 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (w = x → ((y ∈ w ∧ w ∈ z) ↔ (y ∈ x ∧ x ∈ z))))
26	4, 13, 25	cbvexd 978	. . . . . . . . . 10 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → (∃w(y ∈ w ∧ w ∈ z) ↔ ∃x(y ∈ x ∧ x ∈ z)))
27	26	adantr 306	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → (∃w(y ∈ w ∧ w ∈ z) ↔ ∃x(y ∈ x ∧ x ∈ z)))
28	22	a4s 682	. . . . . . . . . 10 ⊢ (∀y w = x → (y ∈ w ↔ y ∈ x))
29	28	adantl 305	. . . . . . . . 9 ⊢ (((¬ ∀x x = y ∧ ¬ ∀x x = z) ∧ ∀y w = x) → (y ∈ w ↔ y ∈ x))
30	27, 29	imbi12d 474	. . . . . . . 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	biald 782	. . . . . . 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 12	. . . . . 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	exp 291	. . . . 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 978	. . . 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 168	. . 3 ⊢ ((¬ ∀x x = y ∧ ¬ ∀x x = z) → ∃x∀y(∃x(y ∈ x ∧ x ∈ z) → y &iðin; x))
36	35	exp 291	. 2 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → ∃x∀y(∃x(y ∈ x ∧ x ∈ z) → y ∈ x)))
37		eq5 824	. . . 4 ⊢ (∀x x = y → ∀y∀x x = y)
38		eq5 824	. . . . . 6 ⊢ (∀x x = y → ∀x∀x x = y)
39		eirrv 3449	. . . . . . . 8 ⊢ ¬ y ∈ y
40		a14b 820	. . . . . . . . 9 ⊢ (x = y → (y ∈ x ↔ y ∈ y))
41		pm3.26 256	. . . . . . . . 9 ⊢ ((y ∈ x ∧ x ∈ z) → y ∈ x)
42	40, 41	syl5bi 183	. . . . . . . 8 ⊢ (x = y → ((y ∈ x ∧ x ∈ z) → y ∈ y))
43	39, 42	mtoi 94	. . . . . . 7 ⊢ (x = y → ¬ (y ∈ x ∧ x ∈ z))
44	43	a4s 682	. . . . . 6 ⊢ (∀x x = y → ¬ (y ∈ x ∧ x ∈ z))
45	38, 44	nexd 780	. . . . 5 ⊢ (∀x x = y → ¬ ∃x(y ∈ x ∧ x ∈ z))
46	45	pm2.21d 74	. . . 4 ⊢ (∀x x = y → (∃x(y ∈ x ∧ x ∈ z) → y ∈ x))
47	37, 46	19.21ai 740	. . 3 ⊢ (∀x x = y → ∀y(∃x(y ∈ x ∧ x ∈ z) → y ∈ x))
48		19.8a 712	. . 3 ⊢ (∀y(∃x(y ∈ x ∧ x ∈ z) → y ∈ x) → ∃x∀y(∃x(y ∈ x ∧ x ∈ z) → y ∈ x))
49	47, 48	syl 12	. 2 ⊢ (∀x x = y → ∃x∀y(∃x(y ∈ x ∧ x ∈ z) → y ∈ x))
50		eq5 824	. . . 4 ⊢ (∀x x = z → ∀y∀x x = z)
51		eq5 824	. . . . . 6 ⊢ (∀x x = z → ∀x∀x x = z)
52		eirrv 3449	. . . . . . . 8 ⊢ ¬ z ∈ z
53		a13b 819	. . . . . . . . 9 ⊢ (x = z → (x ∈ z ↔ z ∈ z))
54		pm3.27 260	. . . . . . . . 9 ⊢ ((y ∈ x ∧ x ∈ z) → x ∈ z)
55	53, 54	syl5bi 183	. . . . . . . 8 ⊢ (x = z → ((y ∈ x ∧ x ∈ z) → z ∈ z))
56	52, 55	mtoi 94	. . . . . . 7 ⊢ (x = z → ¬ (y ∈ x ∧ x ∈ z))
57	56	a4s 682	. . . . . 6 ⊢ (∀x x = z → ¬ (y ∈ x ∧ x ∈ z))
58	51, 57	nexd 780	. . . . 5 ⊢ (∀x x = z → ¬ ∃x(y ∈ x ∧ x ∈ z))
59	58	pm2.21d 74	. . . 4 ⊢ (∀x x = z → (∃x(y ∈ x ∧ x ∈ z) → y ∈ x))
60	50, 59	19.21ai 740	. . 3 ⊢ (∀x x = z → ∀y(∃x(y ∈ x ∧ x ∈ z) → y ∈ x))
61	60, 48	syl 12	. 2 ⊢ (∀x x = z → ∃x∀y(∃x(y ∈ x ∧ x ∈ z) → y ∈ x))
62	36, 49, 61	pm2.61ii 113	1 ⊢ ∃x∀y(∃x(y ∈ x ∧ 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:  zfcndun 3761

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-un 1076  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  df-op 1815  df-br 2063  df-opab 2098  df-eprel 2122  df-fr 2169

metamath.org