Theorem 2eu4 1445

Description: This theorem provides us with a definition of double existential uniqueness ("exactly one x and exactly one y"). Naively one might think (incorrectly) that it could be defined by ∃!x∃!yφ. See 2eu1 1442 for a condition under which the naive definition holds and 2exeu 1439 for a one-way implication. See 2eu5 1446 and 2eu8 1449 for alternate definitions.

Assertion

Ref	Expression
2eu4	⊢ ((∃!x∃yφ ⋀ ∃!y∃xφ) ↔ (∃x∃yφ ⋀ ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))))

Distinct variable groups:   x,y,z,w   φ,z,w

Proof of Theorem 2eu4

Step	Hyp	Ref	Expression
1		ax-17 968	. . . 4 ⊢ (∃yφ → ∀z∃yφ)
2	1	eu3 1390	. . 3 ⊢ (∃!x∃yφ ↔ (∃x∃yφ ⋀ ∃z∀x(∃yφ → x = z)))
3		ax-17 968	. . . 4 ⊢ (∃xφ → ∀w∃xφ)
4	3	eu3 1390	. . 3 ⊢ (∃!y∃xφ ↔ (∃y∃xφ ⋀ ∃w∀y(∃xφ → y = w)))
5	2, 4	anbi12i 481	. 2 ⊢ ((∃!x∃yφ ⋀ ∃!y∃xφ) ↔ ((∃x∃yφ ⋀ ∃z∀x(∃yφ → x = z)) ⋀ (∃y∃xφ ⋀ ∃w∀y(∃xφ → y = w))))
6		an4 505	. 2 ⊢ (((∃x∃yφ ⋀ ∃z∀x(∃yφ → x = z)) ⋀ (∃y∃xφ ⋀ ∃w∀y(∃xφ → y = w))) ↔ ((∃x∃yφ ⋀ ∃y∃xφ) ⋀ (∃z∀x(∃yφ → x = z) ⋀ ∃w∀y(∃xφ → y = w))))
7		excom 1042	. . . . 5 ⊢ (∃y∃xφ ↔ ∃x∃yφ)
8	7	anbi2i 479	. . . 4 ⊢ ((∃x∃yφ ⋀ ∃y∃xφ) ↔ (∃x∃yφ ⋀ ∃x∃yφ))
9		anidm 432	. . . 4 ⊢ ((∃x∃yφ ⋀ ∃x∃yφ) ↔ ∃x∃yφ)
10	8, 9	bitr 173	. . 3 ⊢ ((∃x∃yφ ⋀ ∃y∃xφ) ↔ ∃x∃yφ)
11		hba1 1000	. . . . . . . . . 10 ⊢ (∀x∀y(φ → y = w) → ∀x∀x∀y(φ → y = w))
12	11	19.3 1027	. . . . . . . . 9 ⊢ (∀x∀x∀y(φ → y = w) ↔ ∀x∀y(φ → y = w))
13	12	anbi2i 479	. . . . . . . 8 ⊢ ((∀x∀y(φ → x = z) ⋀ ∀x∀x∀y(φ → y = w)) ↔ (∀x∀y(φ → x = z) ⋀ ∀x∀y(φ → y = w)))
14		19.26 1063	. . . . . . . 8 ⊢ (∀x(∀y(φ → x = z) ⋀ ∀x∀y(φ → y = w)) ↔ (∀x∀y(φ → x = z) ⋀ ∀x∀x∀y(φ → y = w)))
15		jcab 596	. . . . . . . . . . . 12 ⊢ ((φ → (x = z ⋀ y = w)) ↔ ((φ → x = z) ⋀ (φ → y = w)))
16	15	albii 996	. . . . . . . . . . 11 ⊢ (∀y(φ → (x = z ⋀ y = w)) ↔ ∀y((φ → x = z) ⋀ (φ → y = w)))
17		19.26 1063	. . . . . . . . . . 11 ⊢ (∀y((φ → x = z) ⋀ (φ → y = w)) ↔ (∀y(φ → x = z) ⋀ ∀y(φ → y = w)))
18	16, 17	bitr 173	. . . . . . . . . 10 ⊢ (∀y(φ → (x = z ⋀ y = w)) ↔ (∀y(φ → x = z) ⋀ ∀y(φ → y = w)))
19	18	albii 996	. . . . . . . . 9 ⊢ (∀x∀y(φ → (x = z ⋀ y = w)) ↔ ∀x(∀y(φ → x = z) ⋀ ∀y(φ → y = w)))
20		19.26 1063	. . . . . . . . 9 ⊢ (∀x(∀y(φ → x = z) ⋀ ∀y(φ → y = w)) ↔ (∀x∀y(φ → x = z) ⋀ ∀x∀y(φ → y = w)))
21	19, 20	bitr 173	. . . . . . . 8 ⊢ (∀x∀y(φ → (x = z ⋀ y = w)) ↔ (∀x∀y(φ → x = z) ⋀ ∀x∀y(φ → y = w)))
22	13, 14, 21	3bitr4r 184	. . . . . . 7 ⊢ (∀x∀y(φ → (x = z ⋀ y = w)) ↔ ∀x(∀y(φ → x = z) ⋀ ∀x∀y(φ → y = w)))
23		19.26 1063	. . . . . . . . 9 ⊢ (∀y(∀y(φ → x = z) ⋀ ∀x(φ → y = w)) ↔ (∀y∀y(φ → x = z) ⋀ ∀y∀x(φ → y = w)))
24		hba1 1000	. . . . . . . . . . 11 ⊢ (∀y(φ → x = z) → ∀y∀y(φ → x = z))
25	24	19.3 1027	. . . . . . . . . 10 ⊢ (∀y∀y(φ → x = z) ↔ ∀y(φ → x = z))
26		alcom 1028	. . . . . . . . . 10 ⊢ (∀y∀x(φ → y = w) ↔ ∀x∀y(φ → y = w))
27	25, 26	anbi12i 481	. . . . . . . . 9 ⊢ ((∀y∀y(φ → x = z) ⋀ ∀y∀x(φ → y = w)) ↔ (∀y(φ → x = z) ⋀ ∀x∀y(φ → y = w)))
28	23, 27	bitr 173	. . . . . . . 8 ⊢ (∀y(∀y(φ → x = z) ⋀ ∀x(φ → y = w)) ↔ (∀y(φ → x = z) ⋀ ∀x∀y(φ → y = w)))
29	28	albii 996	. . . . . . 7 ⊢ (∀x∀y(∀y(φ → x = z) ⋀ ∀x(φ → y = w)) ↔ ∀x(∀y(φ → x = z) ⋀ ∀x∀y(φ → y = w)))
30	22, 29	bitr4 176	. . . . . 6 ⊢ (∀x∀y(φ → (x = z ⋀ y = w)) ↔ ∀x∀y(∀y(φ → x = z) ⋀ ∀x(φ → y = w)))
31		19.23v 1288	. . . . . . . 8 ⊢ (∀y(φ → x = z) ↔ (∃yφ → x = z))
32		19.23v 1288	. . . . . . . 8 ⊢ (∀x(φ → y = w) ↔ (∃xφ → y = w))
33	31, 32	anbi12i 481	. . . . . . 7 ⊢ ((∀y(φ → x = z) ⋀ ∀x(φ → y = w)) ↔ ((∃yφ → x = z) ⋀ (∃xφ → y = w)))
34	33	2albii 997	. . . . . 6 ⊢ (∀x∀y(∀y(φ → x = z) ⋀ ∀x(φ → y = w)) ↔ ∀x∀y((∃yφ → x = z) ⋀ (∃xφ → y = w)))
35		hbe1 1012	. . . . . . . 8 ⊢ (∃yφ → ∀y∃yφ)
36		ax-17 968	. . . . . . . 8 ⊢ (x = z → ∀y x = z)
37	35, 36	hbim 1004	. . . . . . 7 ⊢ ((∃yφ → x = z) → ∀y(∃yφ → x = z))
38		hbe1 1012	. . . . . . . 8 ⊢ (∃xφ → ∀x∃xφ)
39		ax-17 968	. . . . . . . 8 ⊢ (y = w → ∀x y = w)
40	38, 39	hbim 1004	. . . . . . 7 ⊢ ((∃xφ → y = w) → ∀x(∃xφ → y = w))
41	37, 40	aaan 1115	. . . . . 6 ⊢ (∀x∀y((∃yφ → x = z) ⋀ (∃xφ → y = w)) ↔ (∀x(∃yφ → x = z) ⋀ ∀y(∃xφ → y = w)))
42	30, 34, 41	3bitr 177	. . . . 5 ⊢ (∀x∀y(φ → (x = z ⋀ y = w)) ↔ (∀x(∃yφ → x = z) ⋀ ∀y(∃xφ → y = w)))
43	42	2exbii 1048	. . . 4 ⊢ (∃z∃w∀x∀y(φ → (x = z ⋀ y = w)) ↔ ∃z∃w(∀x(∃yφ → x = z) ⋀ ∀y(∃xφ → y = w)))
44		eeanv 1318	. . . 4 ⊢ (∃z∃w(∀x(∃yφ → x = z) ⋀ ∀y(∃xφ → y = w)) ↔ (∃z∀x(∃yφ → x = z) ⋀ ∃w∀y(∃xφ → y = w)))
45	43, 44	bitr2 174	. . 3 ⊢ ((∃z∀x(∃yφ → x = z) ⋀ ∃w∀y(∃xφ → y = w)) ↔ ∃z∃w∀x∀y(φ → (x = z ⋀ y = w)))
46	10, 45	anbi12i 481	. 2 ⊢ (((∃x∃yφ ⋀ ∃y∃xφ) ⋀ (∃z∀x(∃yφ → x = z) ⋀ ∃w∀y(∃xφ → y = w))) ↔ (∃x∃yφ ⋀ ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))))
47	5, 6, 46	3bitr 177	1 ⊢ ((∃!x∃yφ ⋀ ∃!y∃xφ) ↔ (∃x∃yφ ⋀ ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 951   = wceq 953  ∃wex 977  ∃!weu 1373

This theorem is referenced by:  2eu5 1446  2eu6 1447

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-11 964  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375

Copyright terms: Public domain