Theorem 2mo 2551

Description: Two equivalent expressions for double "at most one." (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 2-Nov-2019.)

Assertion

Ref	Expression
2mo	⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤   𝜑,𝑧,𝑤

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem 2mo

Step	Hyp	Ref	Expression
1		2mo2 2550	. . . 4 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) ↔ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
2		nfmo1 2481	. . . . . . 7 ⊢ Ⅎ𝑥∃*𝑥∃𝑦𝜑
3		nfe1 2027	. . . . . . . 8 ⊢ Ⅎ𝑥∃𝑥𝜑
4	3	nfmo 2487	. . . . . . 7 ⊢ Ⅎ𝑥∃*𝑦∃𝑥𝜑
5	2, 4	nfan 1828	. . . . . 6 ⊢ Ⅎ𝑥(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑)
6		nfe1 2027	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑦𝜑
7	6	nfmo 2487	. . . . . . . 8 ⊢ Ⅎ𝑦∃*𝑥∃𝑦𝜑
8		nfmo1 2481	. . . . . . . 8 ⊢ Ⅎ𝑦∃*𝑦∃𝑥𝜑
9	7, 8	nfan 1828	. . . . . . 7 ⊢ Ⅎ𝑦(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑)
10		19.8a 2052	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑦𝜑)
11		spsbe 1884	. . . . . . . . . 10 ⊢ ([𝑤 / 𝑦]𝜑 → ∃𝑦𝜑)
12	11	sbimi 1886	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑧 / 𝑥]∃𝑦𝜑)
13		nfv 1843	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧∃𝑦𝜑
14	13	mo3 2507	. . . . . . . . . . 11 ⊢ (∃*𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
15	14	biimpi 206	. . . . . . . . . 10 ⊢ (∃*𝑥∃𝑦𝜑 → ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
16	15	19.21bbi 2060	. . . . . . . . 9 ⊢ (∃*𝑥∃𝑦𝜑 → ((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
17	10, 12, 16	syl2ani 688	. . . . . . . 8 ⊢ (∃*𝑥∃𝑦𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑥 = 𝑧))
18		19.8a 2052	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥𝜑)
19		sbcom2 2445	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
20		spsbe 1884	. . . . . . . . . . 11 ⊢ ([𝑧 / 𝑥]𝜑 → ∃𝑥𝜑)
21	20	sbimi 1886	. . . . . . . . . 10 ⊢ ([𝑤 / 𝑦][𝑧 / 𝑥]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑)
22	19, 21	sylbi 207	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑)
23		nfv 1843	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤∃𝑥𝜑
24	23	mo3 2507	. . . . . . . . . . 11 ⊢ (∃*𝑦∃𝑥𝜑 ↔ ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
25	24	biimpi 206	. . . . . . . . . 10 ⊢ (∃*𝑦∃𝑥𝜑 → ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
26	25	19.21bbi 2060	. . . . . . . . 9 ⊢ (∃*𝑦∃𝑥𝜑 → ((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
27	18, 22, 26	syl2ani 688	. . . . . . . 8 ⊢ (∃*𝑦∃𝑥𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑦 = 𝑤))
28	17, 27	anim12ii 594	. . . . . . 7 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
29	9, 28	alrimi 2082	. . . . . 6 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
30	5, 29	alrimi 2082	. . . . 5 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
31	30	alrimivv 1856	. . . 4 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
32	1, 31	sylbir 225	. . 3 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
33		nfs1v 2437	. . . . . . . 8 ⊢ Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
34		nfs1v 2437	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
35	34	nfsb 2440	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
36		pm3.21 464	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (𝜑 → (𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)))
37	36	imim1d 82	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
38	35, 37	alimd 2081	. . . . . . . 8 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
39	33, 38	alimd 2081	. . . . . . 7 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
40	39	com12 32	. . . . . 6 ⊢ (∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
41	40	aleximi 1759	. . . . 5 ⊢ (∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
42	41	aleximi 1759	. . . 4 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
43		2nexaln 1757	. . . . . 6 ⊢ (¬ ∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑)
44		2sb8e 2467	. . . . . 6 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
45	43, 44	xchnxbi 322	. . . . 5 ⊢ (¬ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑)
46		pm2.21 120	. . . . . . . . 9 ⊢ (¬ 𝜑 → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
47	46	2alimi 1740	. . . . . . . 8 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
48	47	2eximi 1763	. . . . . . 7 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
49	48	19.23bi 2061	. . . . . 6 ⊢ (∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
50	49	19.23bi 2061	. . . . 5 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
51	45, 50	sylbi 207	. . . 4 ⊢ (¬ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
52	42, 51	pm2.61d1 171	. . 3 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
53	32, 52	impbii 199	. 2 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
54		alrot4 2039	. 2 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
55	53, 54	bitri 264	1 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481  ∃wex 1704  [wsb 1880  ∃*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475

This theorem is referenced by:  2mos  2552