Theorem 2eu6 1447

Description: Two equivalent expressions for double existential uniqueness.

Assertion

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

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

Proof of Theorem 2eu6

Step	Hyp	Ref	Expression
1		2eu4 1445	. 2 ⊢ ((∃!x∃yφ ⋀ ∃!y∃xφ) ↔ (∃x∃yφ ⋀ ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))))
2		19.29r2 1069	. . . 4 ⊢ ((∃z∃w[z / x][w / y]φ ⋀ ∀z∀w∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u))) → ∃z∃w([z / x][w / y]φ ⋀ ∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u))))
3		ax-17 968	. . . . . 6 ⊢ (φ → ∀zφ)
4		ax-17 968	. . . . . 6 ⊢ (φ → ∀wφ)
5		hbs1 1327	. . . . . 6 ⊢ ([z / x][w / y]φ → ∀x[z / x][w / y]φ)
6		hbs1 1327	. . . . . . 7 ⊢ ([w / y]φ → ∀y[w / y]φ)
7	6	hbsb 1328	. . . . . 6 ⊢ ([z / x][w / y]φ → ∀y[z / x][w / y]φ)
8		sbequ12 1177	. . . . . . 7 ⊢ (y = w → (φ ↔ [w / y]φ))
9		sbequ12 1177	. . . . . . 7 ⊢ (x = z → ([w / y]φ ↔ [z / x][w / y]φ))
10	8, 9	sylan9bbr 539	. . . . . 6 ⊢ ((x = z ⋀ y = w) → (φ ↔ [z / x][w / y]φ))
11	3, 4, 5, 7, 10	cbvex2 1312	. . . . 5 ⊢ (∃x∃yφ ↔ ∃z∃w[z / x][w / y]φ)
12		equequ2 1131	. . . . . . . . . 10 ⊢ (z = v → (x = z ↔ x = v))
13		equequ2 1131	. . . . . . . . . 10 ⊢ (w = u → (y = w ↔ y = u))
14	12, 13	bi2anan9 630	. . . . . . . . 9 ⊢ ((z = v ⋀ w = u) → ((x = z ⋀ y = w) ↔ (x = v ⋀ y = u)))
15	14	imbi2d 610	. . . . . . . 8 ⊢ ((z = v ⋀ w = u) → ((φ → (x = z ⋀ y = w)) ↔ (φ → (x = v ⋀ y = u))))
16	15	2albidv 1275	. . . . . . 7 ⊢ ((z = v ⋀ w = u) → (∀x∀y(φ → (x = z ⋀ y = w)) ↔ ∀x∀y(φ → (x = v ⋀ y = u))))
17	16	cbvex2v 1314	. . . . . 6 ⊢ (∃z∃w∀x∀y(φ → (x = z ⋀ y = w)) ↔ ∃v∃u∀x∀y(φ → (x = v ⋀ y = u)))
18		ax-17 968	. . . . . . . 8 ⊢ ((φ → (x = v ⋀ y = u)) → ∀z(φ → (x = v ⋀ y = u)))
19		ax-17 968	. . . . . . . 8 ⊢ ((φ → (x = v ⋀ y = u)) → ∀w(φ → (x = v ⋀ y = u)))
20		ax-17 968	. . . . . . . . 9 ⊢ ((z = v ⋀ w = u) → ∀x(z = v ⋀ w = u))
21	5, 20	hbim 1004	. . . . . . . 8 ⊢ (([z / x][w / y]φ → (z = v ⋀ w = u)) → ∀x([z / x][w / y]φ → (z = v ⋀ w = u)))
22		ax-17 968	. . . . . . . . 9 ⊢ ((z = v ⋀ w = u) → ∀y(z = v ⋀ w = u))
23	7, 22	hbim 1004	. . . . . . . 8 ⊢ (([z / x][w / y]φ → (z = v ⋀ w = u)) → ∀y([z / x][w / y]φ → (z = v ⋀ w = u)))
24		equequ1 1130	. . . . . . . . . 10 ⊢ (x = z → (x = v ↔ z = v))
25		equequ1 1130	. . . . . . . . . 10 ⊢ (y = w → (y = u ↔ w = u))
26	24, 25	bi2anan9 630	. . . . . . . . 9 ⊢ ((x = z ⋀ y = w) → ((x = v ⋀ y = u) ↔ (z = v ⋀ w = u)))
27	10, 26	imbi12d 624	. . . . . . . 8 ⊢ ((x = z ⋀ y = w) → ((φ → (x = v ⋀ y = u)) ↔ ([z / x][w / y]φ → (z = v ⋀ w = u))))
28	18, 19, 21, 23, 27	cbval2 1311	. . . . . . 7 ⊢ (∀x∀y(φ → (x = v ⋀ y = u)) ↔ ∀z∀w([z / x][w / y]φ → (z = v ⋀ w = u)))
29	28	2exbii 1048	. . . . . 6 ⊢ (∃v∃u∀x∀y(φ → (x = v ⋀ y = u)) ↔ ∃v∃u∀z∀w([z / x][w / y]φ → (z = v ⋀ w = u)))
30		2mo 1440	. . . . . 6 ⊢ (∃v∃u∀z∀w([z / x][w / y]φ → (z = v ⋀ w = u)) ↔ ∀z∀w∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u)))
31	17, 29, 30	3bitr 177	. . . . 5 ⊢ (∃z∃w∀x∀y(φ → (x = z ⋀ y = w)) ↔ ∀z∀w∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u)))
32	11, 31	anbi12i 481	. . . 4 ⊢ ((∃x∃yφ ⋀ ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))) ↔ (∃z∃w[z / x][w / y]φ ⋀ ∀z∀w∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u))))
33		2albi 1104	. . . . . . 7 ⊢ (∀x∀y(φ ↔ (x = z ⋀ y = w)) ↔ (∀x∀y(φ → (x = z ⋀ y = w)) ⋀ ∀x∀y((x = z ⋀ y = w) → φ)))
34		ancom 435	. . . . . . 7 ⊢ ((∀x∀y(φ → (x = z ⋀ y = w)) ⋀ ∀x∀y((x = z ⋀ y = w) → φ)) ↔ (∀x∀y((x = z ⋀ y = w) → φ) ⋀ ∀x∀y(φ → (x = z ⋀ y = w))))
35	33, 34	bitr 173	. . . . . 6 ⊢ (∀x∀y(φ ↔ (x = z ⋀ y = w)) ↔ (∀x∀y((x = z ⋀ y = w) → φ) ⋀ ∀x∀y(φ → (x = z ⋀ y = w))))
36	35	2exbii 1048	. . . . 5 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ⋀ y = w)) ↔ ∃z∃w(∀x∀y((x = z ⋀ y = w) → φ) ⋀ ∀x∀y(φ → (x = z ⋀ y = w))))
37		equcom 1125	. . . . . . . . . . . . 13 ⊢ (z = x ↔ x = z)
38		equcom 1125	. . . . . . . . . . . . 13 ⊢ (w = y ↔ y = w)
39	37, 38	anbi12i 481	. . . . . . . . . . . 12 ⊢ ((z = x ⋀ w = y) ↔ (x = z ⋀ y = w))
40	39	imbi2i 185	. . . . . . . . . . 11 ⊢ ((([z / x][w / y]φ ⋀ φ) → (z = x ⋀ w = y)) ↔ (([z / x][w / y]φ ⋀ φ) → (x = z ⋀ y = w)))
41		impexp 347	. . . . . . . . . . 11 ⊢ ((([z / x][w / y]φ ⋀ φ) → (x = z ⋀ y = w)) ↔ ([z / x][w / y]φ → (φ → (x = z ⋀ y = w))))
42	40, 41	bitr 173	. . . . . . . . . 10 ⊢ ((([z / x][w / y]φ ⋀ φ) → (z = x ⋀ w = y)) ↔ ([z / x][w / y]φ → (φ → (x = z ⋀ y = w))))
43	42	2albii 997	. . . . . . . . 9 ⊢ (∀x∀y(([z / x][w / y]φ ⋀ φ) → (z = x ⋀ w = y)) ↔ ∀x∀y([z / x][w / y]φ → (φ → (x = z ⋀ y = w))))
44		ax-17 968	. . . . . . . . . 10 ⊢ ((([z / x][w / y]φ ⋀ φ) → (z = x ⋀ w = y)) → ∀v(([z / x][w / y]φ ⋀ φ) → (z = x ⋀ w = y)))
45		ax-17 968	. . . . . . . . . 10 ⊢ ((([z / x][w / y]φ ⋀ φ) → (z = x ⋀ w = y)) → ∀u(([z / x][w / y]φ ⋀ φ) → (z = x ⋀ w = y)))
46	5	hbsb 1328	. . . . . . . . . . . . 13 ⊢ ([u / w][z / x][w / y]φ → ∀x[u / w][z / x][w / y]φ)
47	46	hbsb 1328	. . . . . . . . . . . 12 ⊢ ([v / z][u / w][z / x][w / y]φ → ∀x[v / z][u / w][z / x][w / y]φ)
48	5, 47	hban 1006	. . . . . . . . . . 11 ⊢ (([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → ∀x([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ))
49	48, 20	hbim 1004	. . . . . . . . . 10 ⊢ ((([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u)) → ∀x(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u)))
50	7	hbsb 1328	. . . . . . . . . . . . 13 ⊢ ([u / w][z / x][w / y]φ → ∀y[u / w][z / x][w / y]φ)
51	50	hbsb 1328	. . . . . . . . . . . 12 ⊢ ([v / z][u / w][z / x][w / y]φ → ∀y[v / z][u / w][z / x][w / y]φ)
52	7, 51	hban 1006	. . . . . . . . . . 11 ⊢ (([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → ∀y([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ))
53	52, 22	hbim 1004	. . . . . . . . . 10 ⊢ ((([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u)) → ∀y(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u)))
54		sbequ12 1177	. . . . . . . . . . . . . 14 ⊢ (y = u → (φ ↔ [u / y]φ))
55		sbequ12 1177	. . . . . . . . . . . . . 14 ⊢ (x = v → ([u / y]φ ↔ [v / x][u / y]φ))
56	54, 55	sylan9bbr 539	. . . . . . . . . . . . 13 ⊢ ((x = v ⋀ y = u) → (φ ↔ [v / x][u / y]φ))
57		ax-17 968	. . . . . . . . . . . . . . 15 ⊢ ([u / w][w / y]φ → ∀z[u / w][w / y]φ)
58	57	sbco2 1250	. . . . . . . . . . . . . 14 ⊢ ([v / z][z / x][u / w][w / y]φ ↔ [v / x][u / w][w / y]φ)
59		sbcom2 1329	. . . . . . . . . . . . . . 15 ⊢ ([z / x][u / w][w / y]φ ↔ [u / w][z / x][w / y]φ)
60	59	sbbii 1170	. . . . . . . . . . . . . 14 ⊢ ([v / z][z / x][u / w][w / y]φ ↔ [v / z][u / w][z / x][w / y]φ)
61	4	sbco2 1250	. . . . . . . . . . . . . . 15 ⊢ ([u / w][w / y]φ ↔ [u / y]φ)
62	61	sbbii 1170	. . . . . . . . . . . . . 14 ⊢ ([v / x][u / w][w / y]φ ↔ [v / x][u / y]φ)
63	58, 60, 62	3bitr3r 182	. . . . . . . . . . . . 13 ⊢ ([v / x][u / y]φ ↔ [v / z][u / w][z / x][w / y]φ)
64	56, 63	syl6bb 534	. . . . . . . . . . . 12 ⊢ ((x = v ⋀ y = u) → (φ ↔ [v / z][u / w][z / x][w / y]φ))
65	64	anbi2d 614	. . . . . . . . . . 11 ⊢ ((x = v ⋀ y = u) → (([z / x][w / y]φ ⋀ φ) ↔ ([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ)))
66		equequ2 1131	. . . . . . . . . . . 12 ⊢ (x = v → (z = x ↔ z = v))
67		equequ2 1131	. . . . . . . . . . . 12 ⊢ (y = u → (w = y ↔ w = u))
68	66, 67	bi2anan9 630	. . . . . . . . . . 11 ⊢ ((x = v ⋀ y = u) → ((z = x ⋀ w = y) ↔ (z = v ⋀ w = u)))
69	65, 68	imbi12d 624	. . . . . . . . . 10 ⊢ ((x = v ⋀ y = u) → ((([z / x][w / y]φ ⋀ φ) → (z = x ⋀ w = y)) ↔ (([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u))))
70	44, 45, 49, 53, 69	cbval2 1311	. . . . . . . . 9 ⊢ (∀x∀y(([z / x][w / y]φ ⋀ φ) → (z = x ⋀ w = y)) ↔ ∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u)))
71	5, 7	19.21-2 1053	. . . . . . . . 9 ⊢ (∀x∀y([z / x][w / y]φ → (φ → (x = z ⋀ y = w))) ↔ ([z / x][w / y]φ → ∀x∀y(φ → (x = z ⋀ y = w))))
72	43, 70, 71	3bitr3 181	. . . . . . . 8 ⊢ (∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u)) ↔ ([z / x][w / y]φ → ∀x∀y(φ → (x = z ⋀ y = w))))
73	72	anbi2i 479	. . . . . . 7 ⊢ (([z / x][w / y]φ ⋀ ∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u))) ↔ ([z / x][w / y]φ ⋀ ([z / x][w / y]φ → ∀x∀y(φ → (x = z ⋀ y = w)))))
74		abai 478	. . . . . . 7 ⊢ (([z / x][w / y]φ ⋀ ∀x∀y(φ → (x = z ⋀ y = w))) ↔ ([z / x][w / y]φ ⋀ ([z / x][w / y]φ → ∀x∀y(φ → (x = z ⋀ y = w)))))
75		2sb6 1331	. . . . . . . 8 ⊢ ([z / x][w / y]φ ↔ ∀x∀y((x = z ⋀ y = w) → φ))
76	75	anbi1i 480	. . . . . . 7 ⊢ (([z / x][w / y]φ ⋀ ∀x∀y(φ → (x = z ⋀ y = w))) ↔ (∀x∀y((x = z ⋀ y = w) → φ) ⋀ ∀x∀y(φ → (x = z ⋀ y = w))))
77	73, 74, 76	3bitr2 179	. . . . . 6 ⊢ (([z / x][w / y]φ ⋀ ∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u))) ↔ (∀x∀y((x = z ⋀ y = w) → φ) ⋀ ∀x∀y(φ → (x = z ⋀ y = w))))
78	77	2exbii 1048	. . . . 5 ⊢ (∃z∃w([z / x][w / y]φ ⋀ ∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u))) ↔ ∃z∃w(∀x∀y((x = z ⋀ y = w) → φ) ⋀ ∀x∀y(φ → (x = z ⋀ y = w))))
79	36, 78	bitr4 176	. . . 4 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ⋀ y = w)) ↔ ∃z∃w([z / x][w / y]φ ⋀ ∀v∀u(([z / x][w / y]φ ⋀ [v / z][u / w][z / x][w / y]φ) → (z = v ⋀ w = u))))
80	2, 32, 79	3imtr4 219	. . 3 ⊢ ((∃x∃yφ ⋀ ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))) → ∃z∃w∀x∀y(φ ↔ (x = z ⋀ y = w)))
81		bi2 149	. . . . . . 7 ⊢ ((φ ↔ (x = z ⋀ y = w)) → ((x = z ⋀ y = w) → φ))
82	81	19.20i2 990	. . . . . 6 ⊢ (∀x∀y(φ ↔ (x = z ⋀ y = w)) → ∀x∀y((x = z ⋀ y = w) → φ))
83	82	19.22i2 1037	. . . . 5 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ⋀ y = w)) → ∃z∃w∀x∀y((x = z ⋀ y = w) → φ))
84		2exsb 1346	. . . . 5 ⊢ (∃x∃yφ ↔ ∃z∃w∀x∀y((x = z ⋀ y = w) → φ))
85	83, 84	sylibr 200	. . . 4 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ⋀ y = w)) → ∃x∃yφ)
86		bi1 148	. . . . . 6 ⊢ ((φ ↔ (x = z ⋀ y = w)) → (φ → (x = z ⋀ y = w)))
87	86	19.20i2 990	. . . . 5 ⊢ (∀x∀y(φ ↔ (x = z ⋀ y = w)) → ∀x∀y(φ → (x = z ⋀ y = w)))
88	87	19.22i2 1037	. . . 4 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ⋀ y = w)) → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w)))
89	85, 88	jca 288	. . 3 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ⋀ y = w)) → (∃x∃yφ ⋀ ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))))
90	80, 89	impbi 157	. 2 ⊢ ((∃x∃yφ ⋀ ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))) ↔ ∃z∃w∀x∀y(φ ↔ (x = z ⋀ y = w)))
91	1, 90	bitr 173	1 ⊢ ((∃!x∃yφ ⋀ ∃!y∃xφ) ↔ ∃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 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-9 962  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