Metamath Proof Explorer

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 A <-> A = (/) )

Proof

Step Hyp Ref Expression
1 equid 
 |-  x = x
2 vex 
 |-  x e. _V
3 2 ideq 
 |-  ( x _I x <-> x = x )
4 1 3 mpbir 
 |-  x _I x
5 poirr 
 |-  ( ( _I Po A /\ x e. A ) -> -. x _I x )
6 5 ex 
 |-  ( _I Po A -> ( x e. A -> -. x _I x ) )
7 4 6 mt2i 
 |-  ( _I Po A -> -. x e. A )
8 7 eq0rdv 
 |-  ( _I Po A -> A = (/) )
9 po0 
 |-  _I Po (/)
10 poeq2 
 |-  ( A = (/) -> ( _I Po A <-> _I Po (/) ) )
11 9 10 mpbiri 
 |-  ( A = (/) -> _I Po A )
12 8 11 impbii 
 |-  ( _I Po A <-> A = (/) )