Theorem 2mo 2539

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 2538	. . . 4 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) ↔ ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
2		nfmo1 2469	. . . . . . 7 ⊢ Ⅎ𝑥∃*𝑥∃𝑦𝜑
3		nfe1 2014	. . . . . . . 8 ⊢ Ⅎ𝑥∃𝑥𝜑
4	3	nfmo 2475	. . . . . . 7 ⊢ Ⅎ𝑥∃*𝑦∃𝑥𝜑
5	2, 4	nfan 1816	. . . . . 6 ⊢ Ⅎ𝑥(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑)
6		nfe1 2014	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑦𝜑
7	6	nfmo 2475	. . . . . . . 8 ⊢ Ⅎ𝑦∃*𝑥∃𝑦𝜑
8		nfmo1 2469	. . . . . . . 8 ⊢ Ⅎ𝑦∃*𝑦∃𝑥𝜑
9	7, 8	nfan 1816	. . . . . . 7 ⊢ Ⅎ𝑦(∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑)
10		19.8a 2039	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑦𝜑)
11		spsbe 1871	. . . . . . . . . 10 ⊢ ([𝑤 / 𝑦]𝜑 → ∃𝑦𝜑)
12	11	sbimi 1873	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑧 / 𝑥]∃𝑦𝜑)
13		nfv 1830	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧∃𝑦𝜑
14	13	mo3 2495	. . . . . . . . . . 11 ⊢ (∃*𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
15	14	biimpi 205	. . . . . . . . . 10 ⊢ (∃*𝑥∃𝑦𝜑 → ∀𝑥∀𝑧((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
16	15	19.21bbi 2048	. . . . . . . . 9 ⊢ (∃*𝑥∃𝑦𝜑 → ((∃𝑦𝜑 ∧ [𝑧 / 𝑥]∃𝑦𝜑) → 𝑥 = 𝑧))
17	10, 12, 16	syl2ani 686	. . . . . . . 8 ⊢ (∃*𝑥∃𝑦𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑥 = 𝑧))
18		19.8a 2039	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥𝜑)
19		sbcom2 2433	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
20		spsbe 1871	. . . . . . . . . . 11 ⊢ ([𝑧 / 𝑥]𝜑 → ∃𝑥𝜑)
21	20	sbimi 1873	. . . . . . . . . 10 ⊢ ([𝑤 / 𝑦][𝑧 / 𝑥]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑)
22	19, 21	sylbi 206	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → [𝑤 / 𝑦]∃𝑥𝜑)
23		nfv 1830	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤∃𝑥𝜑
24	23	mo3 2495	. . . . . . . . . . 11 ⊢ (∃*𝑦∃𝑥𝜑 ↔ ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
25	24	biimpi 205	. . . . . . . . . 10 ⊢ (∃*𝑦∃𝑥𝜑 → ∀𝑦∀𝑤((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
26	25	19.21bbi 2048	. . . . . . . . 9 ⊢ (∃*𝑦∃𝑥𝜑 → ((∃𝑥𝜑 ∧ [𝑤 / 𝑦]∃𝑥𝜑) → 𝑦 = 𝑤))
27	18, 22, 26	syl2ani 686	. . . . . . . 8 ⊢ (∃*𝑦∃𝑥𝜑 → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → 𝑦 = 𝑤))
28	17, 27	anim12ii 592	. . . . . . 7 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
29	9, 28	alrimi 2069	. . . . . 6 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
30	5, 29	alrimi 2069	. . . . 5 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
31	30	alrimivv 1843	. . . 4 ⊢ ((∃*𝑥∃𝑦𝜑 ∧ ∃*𝑦∃𝑥𝜑) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
32	1, 31	sylbir 224	. . 3 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
33		nfs1v 2425	. . . . . . . 8 ⊢ Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
34		nfs1v 2425	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
35	34	nfsb 2428	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
36		pm3.21 463	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (𝜑 → (𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)))
37	36	imim1d 80	. . . . . . . . 9 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
38	35, 37	alimd 2068	. . . . . . . 8 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
39	33, 38	alimd 2068	. . . . . . 7 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → (∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
40	39	com12 32	. . . . . 6 ⊢ (∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
41	40	aleximi 1749	. . . . 5 ⊢ (∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
42	41	aleximi 1749	. . . 4 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → (∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))))
43		2nexaln 1747	. . . . . 6 ⊢ (¬ ∃𝑥∃𝑦𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑)
44		2sb8e 2455	. . . . . 6 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
45	43, 44	xchnxbi 321	. . . . 5 ⊢ (¬ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦 ¬ 𝜑)
46		pm2.21 119	. . . . . . . . 9 ⊢ (¬ 𝜑 → (𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
47	46	2alimi 1731	. . . . . . . 8 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 → ∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
48	47	2eximi 1753	. . . . . . 7 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
49	48	19.23bi 2049	. . . . . 6 ⊢ (∃𝑤∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
50	49	19.23bi 2049	. . . . 5 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
51	45, 50	sylbi 206	. . . 4 ⊢ (¬ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑 → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
52	42, 51	pm2.61d1 170	. . 3 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) → ∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
53	32, 52	impbii 198	. 2 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
54		alrot4 2026	. 2 ⊢ (∀𝑧∀𝑤∀𝑥∀𝑦((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))
55	53, 54	bitri 263	1 ⊢ (∃𝑧∃𝑤∀𝑥∀𝑦(𝜑 → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∀𝑥∀𝑦∀𝑧∀𝑤((𝜑 ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑) → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695  [wsb 1867  ∃*wmo 2459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463

This theorem is referenced by:  2mos  2540