Theorem 2mo 2647

Description: Two ways of expressing "there exists at most one ordered pair ⟨𝑥, 𝑦⟩ such that 𝜑(𝑥, 𝑦) holds. See also 2mo2 2646. (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 2646	. . . 4 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) ↔ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
2		nfmo1 2556	. . . . . . 7 ⊢ Ⅎ𝑥∃*𝑥∃𝑦𝜑
3		nfe1 2149	. . . . . . . 8 ⊢ Ⅎ𝑥∃𝑥𝜑
4	3	nfmov 2559	. . . . . . 7 ⊢ Ⅎ𝑥∃*𝑦∃𝑥𝜑
5	2, 4	nfan 1898	. . . . . 6 ⊢ Ⅎ𝑥(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑)
6		nfe1 2149	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑦𝜑
7	6	nfmov 2559	. . . . . . . 8 ⊢ Ⅎ𝑦∃*𝑥∃𝑦𝜑
8		nfmo1 2556	. . . . . . . 8 ⊢ Ⅎ𝑦∃*𝑦∃𝑥𝜑
9	7, 8	nfan 1898	. . . . . . 7 ⊢ Ⅎ𝑦(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑)
10		19.8a 2180	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑦𝜑)
11		spsbe 2081	. . . . . . . . . 10 ⊢ ([𝑤 / 𝑦]𝜑 → ∃𝑦𝜑)
12	11	sbimi 2073	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑧 / 𝑥]∃𝑦𝜑)
13		nfv 1913	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧∃𝑦𝜑
14	13	mo3 2563	. . . . . . . . . . 11 ⊢ (∃*𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
15	14	biimpi 216	. . . . . . . . . 10 ⊢ (∃*𝑥∃𝑦𝜑 → ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
16	15	19.21bbi 2189	. . . . . . . . 9 ⊢ (∃*𝑥∃𝑦𝜑 → ((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
17	10, 12, 16	syl2ani 607	. . . . . . . 8 ⊢ (∃*𝑥∃𝑦𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑥 = 𝑧))
18		19.8a 2180	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥𝜑)
19		sbcom2 2172	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
20		spsbe 2081	. . . . . . . . . . 11 ⊢ ([𝑧 / 𝑥]𝜑 → ∃𝑥𝜑)
21	20	sbimi 2073	. . . . . . . . . 10 ⊢ ([𝑤 / 𝑦][𝑧 / 𝑥]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑)
22	19, 21	sylbi 217	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑)
23		nfv 1913	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤∃𝑥𝜑
24	23	mo3 2563	. . . . . . . . . . 11 ⊢ (∃*𝑦∃𝑥𝜑 ↔ ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
25	24	biimpi 216	. . . . . . . . . 10 ⊢ (∃*𝑦∃𝑥𝜑 → ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
26	25	19.21bbi 2189	. . . . . . . . 9 ⊢ (∃*𝑦∃𝑥𝜑 → ((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
27	18, 22, 26	syl2ani 607	. . . . . . . 8 ⊢ (∃*𝑦∃𝑥𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑦 = 𝑤))
28	17, 27	anim12ii 618	. . . . . . 7 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
29	9, 28	alrimi 2212	. . . . . 6 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
30	5, 29	alrimi 2212	. . . . 5 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
31	30	alrimivv 1927	. . . 4 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
32	1, 31	sylbir 235	. . 3 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
33		nfs1v 2155	. . . . . . . 8 ⊢ Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
34		nfs1v 2155	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
35	34	nfsbv 2329	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
36		pm3.21 471	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (𝜑 → (𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)))
37	36	imim1d 82	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
38	35, 37	alimd 2211	. . . . . . . 8 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
39	33, 38	alimd 2211	. . . . . . 7 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
40	39	com12 32	. . . . . 6 ⊢ (∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
41	40	aleximi 1831	. . . . 5 ⊢ (∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
42	41	aleximi 1831	. . . 4 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
43		2nexaln 1829	. . . . . 6 ⊢ (¬ ∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑)
44		nfv 1913	. . . . . . 7 ⊢ Ⅎ𝑤𝜑
45		nfv 1913	. . . . . . 7 ⊢ Ⅎ𝑧𝜑
46	44, 45	2sb8ef 2358	. . . . . 6 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
47	43, 46	xchnxbi 332	. . . . 5 ⊢ (¬ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑)
48		pm2.21 123	. . . . . . . . 9 ⊢ (¬ 𝜑 → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
49	48	2alimi 1811	. . . . . . . 8 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
50	49	2eximi 1835	. . . . . . 7 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
51	50	19.23bi 2190	. . . . . 6 ⊢ (∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
52	51	19.23bi 2190	. . . . 5 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
53	47, 52	sylbi 217	. . . 4 ⊢ (¬ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
54	42, 53	pm2.61d1 180	. . 3 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
55	32, 54	impbii 209	. 2 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
56		alrot4 2160	. 2 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
57	55, 56	bitri 275	1 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1537  ∃wex 1778  [wsb 2063  ∃*wmo 2537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-10 2140  ax-11 2156  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539

This theorem is referenced by:  2mos  2648  2mosOLD  2649