2mo

Description: Two ways of expressing "there exists at most one ordered pair <. x , y >. such that ph ( x , y ) holds. See also 2mo2 . (Contributed by NM, 2-Feb-2005) (Revised by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 2-Nov-2019)

		Ref	Expression
	Assertion	2mo	$⊢ \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w)) \leftrightarrow \forall x \forall y \forall z \forall w ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w))$

Proof

Step	Hyp	Ref	Expression
1		2mo2	$⊢ (\exists^{} x \exists y φ \land \exists^{} y \exists x φ) \leftrightarrow \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w))$
2		nfmo1	$⊢ Ⅎ x \exists^{*} x \exists y φ$
3		nfe1	$⊢ Ⅎ x \exists x φ$
4	3	nfmov	$⊢ Ⅎ x \exists^{*} y \exists x φ$
5	2 4	nfan	$⊢ Ⅎ x (\exists^{} x \exists y φ \land \exists^{} y \exists x φ)$
6		nfe1	$⊢ Ⅎ y \exists y φ$
7	6	nfmov	$⊢ Ⅎ y \exists^{*} x \exists y φ$
8		nfmo1	$⊢ Ⅎ y \exists^{*} y \exists x φ$
9	7 8	nfan	$⊢ Ⅎ y (\exists^{} x \exists y φ \land \exists^{} y \exists x φ)$
10		19.8a	$⊢ φ \to \exists y φ$
11		spsbe	$⊢ [w/ y] φ \to \exists y φ$
12	11	sbimi	$⊢ [z/ x] [w/ y] φ \to [z/ x] \exists y φ$
13		nfv	$⊢ Ⅎ z \exists y φ$
14	13	mo3	$⊢ \exists^{*} x \exists y φ \leftrightarrow \forall x \forall z ((\exists y φ \land [z/ x] \exists y φ) \to x = z)$
15	14	biimpi	$⊢ \exists^{*} x \exists y φ \to \forall x \forall z ((\exists y φ \land [z/ x] \exists y φ) \to x = z)$
16	15	19.21bbi	$⊢ \exists^{*} x \exists y φ \to ((\exists y φ \land [z/ x] \exists y φ) \to x = z)$
17	10 12 16	syl2ani	$⊢ \exists^{*} x \exists y φ \to ((φ \land [z/ x] [w/ y] φ) \to x = z)$
18		19.8a	$⊢ φ \to \exists x φ$
19		sbcom2	$⊢ [z/ x] [w/ y] φ \leftrightarrow [w/ y] [z/ x] φ$
20		spsbe	$⊢ [z/ x] φ \to \exists x φ$
21	20	sbimi	$⊢ [w/ y] [z/ x] φ \to [w/ y] \exists x φ$
22	19 21	sylbi	$⊢ [z/ x] [w/ y] φ \to [w/ y] \exists x φ$
23		nfv	$⊢ Ⅎ w \exists x φ$
24	23	mo3	$⊢ \exists^{*} y \exists x φ \leftrightarrow \forall y \forall w ((\exists x φ \land [w/ y] \exists x φ) \to y = w)$
25	24	biimpi	$⊢ \exists^{*} y \exists x φ \to \forall y \forall w ((\exists x φ \land [w/ y] \exists x φ) \to y = w)$
26	25	19.21bbi	$⊢ \exists^{*} y \exists x φ \to ((\exists x φ \land [w/ y] \exists x φ) \to y = w)$
27	18 22 26	syl2ani	$⊢ \exists^{*} y \exists x φ \to ((φ \land [z/ x] [w/ y] φ) \to y = w)$
28	17 27	anim12ii	$⊢ (\exists^{} x \exists y φ \land \exists^{} y \exists x φ) \to ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w))$
29	9 28	alrimi	$⊢ (\exists^{} x \exists y φ \land \exists^{} y \exists x φ) \to \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w))$
30	5 29	alrimi	$⊢ (\exists^{} x \exists y φ \land \exists^{} y \exists x φ) \to \forall x \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w))$
31	30	alrimivv	$⊢ (\exists^{} x \exists y φ \land \exists^{} y \exists x φ) \to \forall z \forall w \forall x \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w))$
32	1 31	sylbir	$⊢ \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w)) \to \forall z \forall w \forall x \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w))$
33		nfs1v	$⊢ Ⅎ x [z/ x] [w/ y] φ$
34		nfs1v	$⊢ Ⅎ y [w/ y] φ$
35	34	nfsbv	$⊢ Ⅎ y [z/ x] [w/ y] φ$
36		pm3.21	$⊢ [z/ x] [w/ y] φ \to (φ \to (φ \land [z/ x] [w/ y] φ))$
37	36	imim1d	$⊢ [z/ x] [w/ y] φ \to (((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \to (φ \to (x = z \land y = w)))$
38	35 37	alimd	$⊢ [z/ x] [w/ y] φ \to (\forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \to \forall y (φ \to (x = z \land y = w)))$
39	33 38	alimd	$⊢ [z/ x] [w/ y] φ \to (\forall x \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \to \forall x \forall y (φ \to (x = z \land y = w)))$
40	39	com12	$⊢ \forall x \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \to ([z/ x] [w/ y] φ \to \forall x \forall y (φ \to (x = z \land y = w)))$
41	40	aleximi	$⊢ \forall w \forall x \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \to (\exists w [z/ x] [w/ y] φ \to \exists w \forall x \forall y (φ \to (x = z \land y = w)))$
42	41	aleximi	$⊢ \forall z \forall w \forall x \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \to (\exists z \exists w [z/ x] [w/ y] φ \to \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w)))$
43		2nexaln	$⊢ \neg \exists x \exists y φ \leftrightarrow \forall x \forall y \neg φ$
44		nfv	$⊢ Ⅎ w φ$
45		nfv	$⊢ Ⅎ z φ$
46	44 45	2sb8ev	$⊢ \exists x \exists y φ \leftrightarrow \exists z \exists w [z/ x] [w/ y] φ$
47	43 46	xchnxbi	$⊢ \neg \exists z \exists w [z/ x] [w/ y] φ \leftrightarrow \forall x \forall y \neg φ$
48		pm2.21	$⊢ \neg φ \to (φ \to (x = z \land y = w))$
49	48	2alimi	$⊢ \forall x \forall y \neg φ \to \forall x \forall y (φ \to (x = z \land y = w))$
50	49	2eximi	$⊢ \exists z \exists w \forall x \forall y \neg φ \to \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w))$
51	50	19.23bi	$⊢ \exists w \forall x \forall y \neg φ \to \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w))$
52	51	19.23bi	$⊢ \forall x \forall y \neg φ \to \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w))$
53	47 52	sylbi	$⊢ \neg \exists z \exists w [z/ x] [w/ y] φ \to \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w))$
54	42 53	pm2.61d1	$⊢ \forall z \forall w \forall x \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \to \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w))$
55	32 54	impbii	$⊢ \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w)) \leftrightarrow \forall z \forall w \forall x \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w))$
56		alrot4	$⊢ \forall z \forall w \forall x \forall y ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w)) \leftrightarrow \forall x \forall y \forall z \forall w ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w))$
57	55 56	bitri	$⊢ \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w)) \leftrightarrow \forall x \forall y \forall z \forall w ((φ \land [z/ x] [w/ y] φ) \to (x = z \land y = w))$

Metamath Proof Explorer

Theorem 2mo

Proof