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	⊢ ( I Po 𝐴 ↔ 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		equid	⊢ 𝑥 = 𝑥
2		vex	⊢ 𝑥 ∈ V
3	2	ideq	⊢ ( 𝑥 I 𝑥 ↔ 𝑥 = 𝑥 )
4	1 3	mpbir	⊢ 𝑥 I 𝑥
5		poirr	⊢ ( ( I Po 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 I 𝑥 )
6	5	ex	⊢ ( I Po 𝐴 → ( 𝑥 ∈ 𝐴 → ¬ 𝑥 I 𝑥 ) )
7	4 6	mt2i	⊢ ( I Po 𝐴 → ¬ 𝑥 ∈ 𝐴 )
8	7	eq0rdv	⊢ ( I Po 𝐴 → 𝐴 = ∅ )
9		po0	⊢ I Po ∅
10		poeq2	⊢ ( 𝐴 = ∅ → ( I Po 𝐴 ↔ I Po ∅ ) )
11	9 10	mpbiri	⊢ ( 𝐴 = ∅ → I Po 𝐴 )
12	8 11	impbii	⊢ ( I Po 𝐴 ↔ 𝐴 = ∅ )