Theorem 2mo 1445

Description: Two equivalent expressions for double "at most one."

Assertion

Ref	Expression
2mo	⊢ (∃z∃w∀x∀y(φ → (x = z ⋀ y = w)) ↔ ∀x∀y∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)))

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

Proof of Theorem 2mo

Step	Hyp	Ref	Expression
1		equequ2 1133	. . . . . . 7 ⊢ (v = z → (x = v ↔ x = z))
2		equequ2 1133	. . . . . . 7 ⊢ (u = w → (y = u ↔ y = w))
3	1, 2	bi2anan9 631	. . . . . 6 ⊢ ((v = z ⋀ u = w) → ((x = v ⋀ y = u) ↔ (x = z ⋀ y = w)))
4	3	imbi2d 611	. . . . 5 ⊢ ((v = z ⋀ u = w) → ((φ → (x = v ⋀ y = u)) ↔ (φ → (x = z ⋀ y = w))))
5	4	2albidv 1278	. . . 4 ⊢ ((v = z ⋀ u = w) → (∀x∀y(φ → (x = v ⋀ y = u)) ↔ ∀x∀y(φ → (x = z ⋀ y = w))))
6	5	cbvex2v 1317	. . 3 ⊢ (∃v∃u∀x∀y(φ → (x = v ⋀ y = u)) ↔ ∃z∃w∀x∀y(φ → (x = z ⋀ y = w)))
7		ax-17 969	. . . . . . . . 9 ⊢ ((φ → (x = v ⋀ y = u)) → ∀z(φ → (x = v ⋀ y = u)))
8		ax-17 969	. . . . . . . . 9 ⊢ ((φ → (x = v ⋀ y = u)) → ∀w(φ → (x = v ⋀ y = u)))
9		hbs1 1330	. . . . . . . . . 10 ⊢ ([z / x][w / y]φ → ∀x[z / x][w / y]φ)
10		ax-17 969	. . . . . . . . . 10 ⊢ ((z = v ⋀ w = u) → ∀x(z = v ⋀ w = u))
11	9, 10	hbim 1005	. . . . . . . . 9 ⊢ (([z / x][w / y]φ → (z = v ⋀ w = u)) → ∀x([z / x][w / y]φ → (z = v ⋀ w = u)))
12		hbs1 1330	. . . . . . . . . . 11 ⊢ ([w / y]φ → ∀y[w / y]φ)
13	12	hbsb 1331	. . . . . . . . . 10 ⊢ ([z / x][w / y]φ → ∀y[z / x][w / y]φ)
14		ax-17 969	. . . . . . . . . 10 ⊢ ((z = v ⋀ w = u) → ∀y(z = v ⋀ w = u))
15	13, 14	hbim 1005	. . . . . . . . 9 ⊢ (([z / x][w / y]φ → (z = v ⋀ w = u)) → ∀y([z / x][w / y]φ → (z = v ⋀ w = u)))
16		sbequ12 1179	. . . . . . . . . . 11 ⊢ (y = w → (φ ↔ [w / y]φ))
17		sbequ12 1179	. . . . . . . . . . 11 ⊢ (x = z → ([w / y]φ ↔ [z / x][w / y]φ))
18	16, 17	sylan9bbr 540	. . . . . . . . . 10 ⊢ ((x = z ⋀ y = w) → (φ ↔ [z / x][w / y]φ))
19		equequ1 1132	. . . . . . . . . . 11 ⊢ (x = z → (x = v ↔ z = v))
20		equequ1 1132	. . . . . . . . . . 11 ⊢ (y = w → (y = u ↔ w = u))
21	19, 20	bi2anan9 631	. . . . . . . . . 10 ⊢ ((x = z ⋀ y = w) → ((x = v ⋀ y = u) ↔ (z = v ⋀ w = u)))
22	18, 21	imbi12d 625	. . . . . . . . 9 ⊢ ((x = z ⋀ y = w) → ((φ → (x = v ⋀ y = u)) ↔ ([z / x][w / y]φ → (z = v ⋀ w = u))))
23	7, 8, 11, 15, 22	cbval2 1314	. . . . . . . 8 ⊢ (∀x∀y(φ → (x = v ⋀ y = u)) ↔ ∀z∀w([z / x][w / y]φ → (z = v ⋀ w = u)))
24	23	biimp 151	. . . . . . 7 ⊢ (∀x∀y(φ → (x = v ⋀ y = u)) → ∀z∀w([z / x][w / y]φ → (z = v ⋀ w = u)))
25	24	ancli 296	. . . . . 6 ⊢ (∀x∀y(φ → (x = v ⋀ y = u)) → (∀x∀y(φ → (x = v ⋀ y = u)) ⋀ ∀z∀w([z / x][w / y]φ → (z = v ⋀ w = u))))
26		alcom 1030	. . . . . . . . 9 ⊢ (∀y∀z∀w((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))) ↔ ∀z∀y∀w((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))))
27	8, 15	aaan 1117	. . . . . . . . . 10 ⊢ (∀y∀w((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))) ↔ (∀y(φ → (x = v ⋀ y = u)) ⋀ ∀w([z / x][w / y]φ → (z = v ⋀ w = u))))
28	27	albii 997	. . . . . . . . 9 ⊢ (∀z∀y∀w((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))) ↔ ∀z(∀y(φ → (x = v ⋀ y = u)) ⋀ ∀w([z / x][w / y]φ → (z = v ⋀ w = u))))
29	26, 28	bitr 173	. . . . . . . 8 ⊢ (∀y∀z∀w((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))) ↔ ∀z(∀y(φ → (x = v ⋀ y = u)) ⋀ ∀w([z / x][w / y]φ → (z = v ⋀ w = u))))
30	29	albii 997	. . . . . . 7 ⊢ (∀x∀y∀z∀w((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))) ↔ ∀x∀z(∀y(φ → (x = v ⋀ y = u)) ⋀ ∀w([z / x][w / y]φ → (z = v ⋀ w = u))))
31		ax-17 969	. . . . . . . 8 ⊢ (∀y(φ → (x = v ⋀ y = u)) → ∀z∀y(φ → (x = v ⋀ y = u)))
32	11	hbal 1003	. . . . . . . 8 ⊢ (∀w([z / x][w / y]φ → (z = v ⋀ w = u)) → ∀x∀w([z / x][w / y]φ → (z = v ⋀ w = u)))
33	31, 32	aaan 1117	. . . . . . 7 ⊢ (∀x∀z(∀y(φ → (x = v ⋀ y = u)) ⋀ ∀w([z / x][w / y]φ → (z = v ⋀ w = u))) ↔ (∀x∀y(φ → (x = v ⋀ y = u)) ⋀ ∀z∀w([z / x][w / y]φ → (z = v ⋀ w = u))))
34	30, 33	bitr 173	. . . . . 6 ⊢ (∀x∀y∀z∀w((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))) ↔ (∀x∀y(φ → (x = v ⋀ y = u)) ⋀ ∀z∀w([z / x][w / y]φ → (z = v ⋀ w = u))))
35	25, 34	sylibr 200	. . . . 5 ⊢ (∀x∀y(φ → (x = v ⋀ y = u)) → ∀x∀y∀z∀w((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))))
36		prth 555	. . . . . . . 8 ⊢ (((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))) → ((φ ⋀ [z / x][w / y]φ) → ((x = v ⋀ y = u) ⋀ (z = v ⋀ w = u))))
37		equtr2 1131	. . . . . . . . . 10 ⊢ ((x = v ⋀ z = v) → x = z)
38		equtr2 1131	. . . . . . . . . 10 ⊢ ((y = u ⋀ w = u) → y = w)
39	37, 38	anim12i 333	. . . . . . . . 9 ⊢ (((x = v ⋀ z = v) ⋀ (y = u ⋀ w = u)) → (x = z ⋀ y = w))
40	39	an4s 508	. . . . . . . 8 ⊢ (((x = v ⋀ y = u) ⋀ (z = v ⋀ w = u)) → (x = z ⋀ y = w))
41	36, 40	syl6 22	. . . . . . 7 ⊢ (((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))) → ((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)))
42	41	19.20i2 991	. . . . . 6 ⊢ (∀z∀w((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))) → ∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)))
43	42	19.20i2 991	. . . . 5 ⊢ (∀x∀y∀z∀w((φ → (x = v ⋀ y = u)) ⋀ ([z / x][w / y]φ → (z = v ⋀ w = u))) → ∀x∀y∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)))
44	35, 43	syl 10	. . . 4 ⊢ (∀x∀y(φ → (x = v ⋀ y = u)) → ∀x∀y∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)))
45	44	19.23aivv 1294	. . 3 ⊢ (∃v∃u∀x∀y(φ → (x = v ⋀ y = u)) → ∀x∀y∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)))
46	6, 45	sylbir 201	. 2 ⊢ (∃z∃w∀x∀y(φ → (x = z ⋀ y = w)) → ∀x∀y∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)))
47		alrot4 1095	. . . . . . 7 ⊢ (∀x∀y∀z∀w([z / x][w / y]φ → (φ → (x = z ⋀ y = w))) ↔ ∀z∀w∀x∀y([z / x][w / y]φ → (φ → (x = z ⋀ y = w))))
48		19.20 992	. . . . . . . . 9 ⊢ (∀y([z / x][w / y]φ → (φ → (x = z ⋀ y = w))) → (∀y[z / x][w / y]φ → ∀y(φ → (x = z ⋀ y = w))))
49	48	19.20ii 993	. . . . . . . 8 ⊢ (∀x∀y([z / x][w / y]φ → (φ → (x = z ⋀ y = w))) → (∀x∀y[z / x][w / y]φ → ∀x∀y(φ → (x = z ⋀ y = w))))
50	49	19.20i2 991	. . . . . . 7 ⊢ (∀z∀w∀x∀y([z / x][w / y]φ → (φ → (x = z ⋀ y = w))) → ∀z∀w(∀x∀y[z / x][w / y]φ → ∀x∀y(φ → (x = z ⋀ y = w))))
51	47, 50	sylbi 199	. . . . . 6 ⊢ (∀x∀y∀z∀w([z / x][w / y]φ → (φ → (x = z ⋀ y = w))) → ∀z∀w(∀x∀y[z / x][w / y]φ → ∀x∀y(φ → (x = z ⋀ y = w))))
52		19.22 1037	. . . . . . 7 ⊢ (∀w(∀x∀y[z / x][w / y]φ → ∀x∀y(φ → (x = z ⋀ y = w))) → (∃w∀x∀y[z / x][w / y]φ → ∃w∀x∀y(φ → (x = z ⋀ y = w))))
53	52	19.20i 990	. . . . . 6 ⊢ (∀z∀w(∀x∀y[z / x][w / y]φ → ∀x∀y(φ → (x = z ⋀ y = w))) → ∀z(∃w∀x∀y[z / x][w / y]φ → ∃w∀x∀y(φ → (x = z ⋀ y = w))))
54		19.22 1037	. . . . . 6 ⊢ (∀z(∃w∀x∀y[z / x][w / y]φ → ∃w∀x∀y(φ → (x = z ⋀ y = w))) → (∃z∃w∀x∀y[z / x][w / y]φ → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))))
55	51, 53, 54	3syl 20	. . . . 5 ⊢ (∀x∀y∀z∀w([z / x][w / y]φ → (φ → (x = z ⋀ y = w))) → (∃z∃w∀x∀y[z / x][w / y]φ → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))))
56	9, 13	19.21ai 996	. . . . . 6 ⊢ ([z / x][w / y]φ → ∀x∀y[z / x][w / y]φ)
57	56	19.22i2 1039	. . . . 5 ⊢ (∃z∃w[z / x][w / y]φ → ∃z∃w∀x∀y[z / x][w / y]φ)
58	55, 57	syl5com 52	. . . 4 ⊢ (∃z∃w[z / x][w / y]φ → (∀x∀y∀z∀w([z / x][w / y]φ → (φ → (x = z ⋀ y = w))) → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))))
59		impexp 347	. . . . . . 7 ⊢ (((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)) ↔ (φ → ([z / x][w / y]φ → (x = z ⋀ y = w))))
60		bi2.04 160	. . . . . . 7 ⊢ ((φ → ([z / x][w / y]φ → (x = z ⋀ y = w))) ↔ ([z / x][w / y]φ → (φ → (x = z ⋀ y = w))))
61	59, 60	bitr 173	. . . . . 6 ⊢ (((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)) ↔ ([z / x][w / y]φ → (φ → (x = z ⋀ y = w))))
62	61	2albii 998	. . . . 5 ⊢ (∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)) ↔ ∀z∀w([z / x][w / y]φ → (φ → (x = z ⋀ y = w))))
63	62	2albii 998	. . . 4 ⊢ (∀x∀y∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)) ↔ ∀x∀y∀z∀w([z / x][w / y]φ → (φ → (x = z ⋀ y = w))))
64	58, 63	syl5ib 206	. . 3 ⊢ (∃z∃w[z / x][w / y]φ → (∀x∀y∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)) → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))))
65		alnex 1031	. . . . . . 7 ⊢ (∀w ¬ [z / x][w / y]φ ↔ ¬ ∃w[z / x][w / y]φ)
66	65	albii 997	. . . . . 6 ⊢ (∀z∀w ¬ [z / x][w / y]φ ↔ ∀z ¬ ∃w[z / x][w / y]φ)
67		alnex 1031	. . . . . 6 ⊢ (∀z ¬ ∃w[z / x][w / y]φ ↔ ¬ ∃z∃w[z / x][w / y]φ)
68	66, 67	bitr 173	. . . . 5 ⊢ (∀z∀w ¬ [z / x][w / y]φ ↔ ¬ ∃z∃w[z / x][w / y]φ)
69		ax-17 969	. . . . . . . 8 ⊢ (¬ φ → ∀z ¬ φ)
70		ax-17 969	. . . . . . . 8 ⊢ (¬ φ → ∀w ¬ φ)
71	9	hbn 1002	. . . . . . . 8 ⊢ (¬ [z / x][w / y]φ → ∀x ¬ [z / x][w / y]φ)
72	13	hbn 1002	. . . . . . . 8 ⊢ (¬ [z / x][w / y]φ → ∀y ¬ [z / x][w / y]φ)
73	18	negbid 610	. . . . . . . 8 ⊢ ((x = z ⋀ y = w) → (¬ φ ↔ ¬ [z / x][w / y]φ))
74	69, 70, 71, 72, 73	cbval2 1314	. . . . . . 7 ⊢ (∀x∀y ¬ φ ↔ ∀z∀w ¬ [z / x][w / y]φ)
75	74	biimpr 152	. . . . . 6 ⊢ (∀z∀w ¬ [z / x][w / y]φ → ∀x∀y ¬ φ)
76		pm2.21 76	. . . . . . 7 ⊢ (¬ φ → (φ → (x = z ⋀ y = w)))
77	76	19.20i2 991	. . . . . 6 ⊢ (∀x∀y ¬ φ → ∀x∀y(φ → (x = z ⋀ y = w)))
78		19.8a 1027	. . . . . . 7 ⊢ (∃w∀x∀y(φ → (x = z ⋀ y = w)) → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w)))
79	78	19.23bi 1063	. . . . . 6 ⊢ (∀x∀y(φ → (x = z ⋀ y = w)) → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w)))
80	75, 77, 79	3syl 20	. . . . 5 ⊢ (∀z∀w ¬ [z / x][w / y]φ → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w)))
81	68, 80	sylbir 201	. . . 4 ⊢ (¬ ∃z∃w[z / x][w / y]φ → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w)))
82	81	a1d 12	. . 3 ⊢ (¬ ∃z∃w[z / x][w / y]φ → (∀x∀y∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)) → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w))))
83	64, 82	pm2.61i 126	. 2 ⊢ (∀x∀y∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)) → ∃z∃w∀x∀y(φ → (x = z ⋀ y = w)))
84	46, 83	impbi 157	1 ⊢ (∃z∃w∀x∀y(φ → (x = z ⋀ y = w)) ↔ ∀x∀y∀z∀w((φ ⋀ [z / x][w / y]φ) → (x = z ⋀ y = w)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954  ∃wex 978  [wsbc 1168

This theorem is referenced by:  2mos 1446  2eu6 1452

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain