modom

Description: Two ways to express "at most one". (Contributed by Stefan O'Rear, 28-Oct-2014)

		Ref	Expression
	Assertion	modom	$⊢ \exists^{*} x φ \leftrightarrow \{x \| φ\} ≼ 1_{𝑜}$

Step	Hyp	Ref	Expression
1		moeu	$⊢ \exists^{*} x φ \leftrightarrow (\exists x φ \to \exists! x φ)$
2		imor	$⊢ (\exists x φ \to \exists! x φ) \leftrightarrow (\neg \exists x φ \lor \exists! x φ)$
3		abn0	$⊢ \{x \| φ\} \neq \emptyset \leftrightarrow \exists x φ$
4	3	necon1bbii	$⊢ \neg \exists x φ \leftrightarrow \{x \| φ\} = \emptyset$
5		sdom1	$⊢ \{x \| φ\} ≺ 1_{𝑜} \leftrightarrow \{x \| φ\} = \emptyset$
6	4 5	bitr4i	$⊢ \neg \exists x φ \leftrightarrow \{x \| φ\} ≺ 1_{𝑜}$
7		euen1	$⊢ \exists! x φ \leftrightarrow \{x \| φ\} \approx 1_{𝑜}$
8	6 7	orbi12i	$⊢ (\neg \exists x φ \lor \exists! x φ) \leftrightarrow (\{x \| φ\} ≺ 1_{𝑜} \lor \{x \| φ\} \approx 1_{𝑜})$
9		brdom2	$⊢ \{x \| φ\} ≼ 1_{𝑜} \leftrightarrow (\{x \| φ\} ≺ 1_{𝑜} \lor \{x \| φ\} \approx 1_{𝑜})$
10	8 9	bitr4i	$⊢ (\neg \exists x φ \lor \exists! x φ) \leftrightarrow \{x \| φ\} ≼ 1_{𝑜}$
11	1 2 10	3bitri	$⊢ \exists^{*} x φ \leftrightarrow \{x \| φ\} ≼ 1_{𝑜}$

Metamath Proof Explorer