2mo2

Description: Two ways of expressing "there exists at most one ordered pair <. x , y >. such that ph ( x , y ) holds. Note that this is not equivalent to E* x E* y ph . See also 2mo . This is the analogue of 2eu4 for existential uniqueness. (Contributed by Wolf Lammen, 26-Oct-2019) Reduce dependencies on axioms. (Revised by Wolf Lammen, 3-Jan-2023)

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		exdistrv	$⊢ \exists z \exists w (\forall x (\exists y φ \to x = z) \land \forall y (\exists x φ \to y = w)) \leftrightarrow (\exists z \forall x (\exists y φ \to x = z) \land \exists w \forall y (\exists x φ \to y = w))$
2		jcab	$⊢ (φ \to (x = z \land y = w)) \leftrightarrow ((φ \to x = z) \land (φ \to y = w))$
3	2	2albii	$⊢ \forall x \forall y (φ \to (x = z \land y = w)) \leftrightarrow \forall x \forall y ((φ \to x = z) \land (φ \to y = w))$
4		19.26-2	$⊢ \forall x \forall y ((φ \to x = z) \land (φ \to y = w)) \leftrightarrow (\forall x \forall y (φ \to x = z) \land \forall x \forall y (φ \to y = w))$
5		19.23v	$⊢ \forall y (φ \to x = z) \leftrightarrow (\exists y φ \to x = z)$
6	5	albii	$⊢ \forall x \forall y (φ \to x = z) \leftrightarrow \forall x (\exists y φ \to x = z)$
7		alcom	$⊢ \forall x \forall y (φ \to y = w) \leftrightarrow \forall y \forall x (φ \to y = w)$
8		19.23v	$⊢ \forall x (φ \to y = w) \leftrightarrow (\exists x φ \to y = w)$
9	8	albii	$⊢ \forall y \forall x (φ \to y = w) \leftrightarrow \forall y (\exists x φ \to y = w)$
10	7 9	bitri	$⊢ \forall x \forall y (φ \to y = w) \leftrightarrow \forall y (\exists x φ \to y = w)$
11	6 10	anbi12i	$⊢ (\forall x \forall y (φ \to x = z) \land \forall x \forall y (φ \to y = w)) \leftrightarrow (\forall x (\exists y φ \to x = z) \land \forall y (\exists x φ \to y = w))$
12	3 4 11	3bitri	$⊢ \forall x \forall y (φ \to (x = z \land y = w)) \leftrightarrow (\forall x (\exists y φ \to x = z) \land \forall y (\exists x φ \to y = w))$
13	12	2exbii	$⊢ \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w)) \leftrightarrow \exists z \exists w (\forall x (\exists y φ \to x = z) \land \forall y (\exists x φ \to y = w))$
14		df-mo	$⊢ \exists^{*} x \exists y φ \leftrightarrow \exists z \forall x (\exists y φ \to x = z)$
15		df-mo	$⊢ \exists^{*} y \exists x φ \leftrightarrow \exists w \forall y (\exists x φ \to y = w)$
16	14 15	anbi12i	$⊢ (\exists^{} x \exists y φ \land \exists^{} y \exists x φ) \leftrightarrow (\exists z \forall x (\exists y φ \to x = z) \land \exists w \forall y (\exists x φ \to y = w))$
17	1 13 16	3bitr4ri	$⊢ (\exists^{} x \exists y φ \land \exists^{} y \exists x φ) \leftrightarrow \exists z \exists w \forall x \forall y (φ \to (x = z \land y = w))$

Metamath Proof Explorer

Theorem 2mo2

Proof