Theorem ipo0

Description: If the identity relation partially orders any class, then that class is the null class. (Contributed by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	ipo0	$$⊢\mathrm{I}\mathrm{Po}A\leftrightarrow A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		equid	$$⊢x=x$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	ideq	$$⊢x\mathrm{I}x\leftrightarrow x=x$$
4	1 3	mpbir	$$⊢x\mathrm{I}x$$
5		poirr	$$⊢\left(\mathrm{I}\mathrm{Po}A\wedge x\in A\right)\to \neg x\mathrm{I}x$$
6	5	ex	$$⊢\mathrm{I}\mathrm{Po}A\to \left(x\in A\to \neg x\mathrm{I}x\right)$$
7	4 6	mt2i	$$⊢\mathrm{I}\mathrm{Po}A\to \neg x\in A$$
8	7	eq0rdv	$$⊢\mathrm{I}\mathrm{Po}A\to A=\varnothing$$
9		po0	$$⊢\mathrm{I}\mathrm{Po}\varnothing$$
10		poeq2	$$⊢A=\varnothing \to \left(\mathrm{I}\mathrm{Po}A\leftrightarrow \mathrm{I}\mathrm{Po}\varnothing \right)$$
11	9 10	mpbiri	$$⊢A=\varnothing \to \mathrm{I}\mathrm{Po}A$$
12	8 11	impbii	$$⊢\mathrm{I}\mathrm{Po}A\leftrightarrow A=\varnothing$$