Metamath Proof Explorer

Theorem sorpss

Description: Express strict ordering under proper subsets, i.e. the notion of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion sorpss 
|- ( [C.] Or A <-> A. x e. A A. y e. A ( x C_ y \/ y C_ x ) )

Proof

Step Hyp Ref Expression
1 porpss 
 |-  [C.] Po A
2 1 biantrur 
 |-  ( A. x e. A A. y e. A ( x [C.] y \/ x = y \/ y [C.] x ) <-> ( [C.] Po A /\ A. x e. A A. y e. A ( x [C.] y \/ x = y \/ y [C.] x ) ) )
3 sspsstri 
 |-  ( ( x C_ y \/ y C_ x ) <-> ( x C. y \/ x = y \/ y C. x ) )
4 vex 
 |-  y e. _V
5 4 brrpss 
 |-  ( x [C.] y <-> x C. y )
6 biid 
 |-  ( x = y <-> x = y )
7 vex 
 |-  x e. _V
8 7 brrpss 
 |-  ( y [C.] x <-> y C. x )
9 5 6 8 3orbi123i 
 |-  ( ( x [C.] y \/ x = y \/ y [C.] x ) <-> ( x C. y \/ x = y \/ y C. x ) )
10 3 9 bitr4i 
 |-  ( ( x C_ y \/ y C_ x ) <-> ( x [C.] y \/ x = y \/ y [C.] x ) )
11 10 2ralbii 
 |-  ( A. x e. A A. y e. A ( x C_ y \/ y C_ x ) <-> A. x e. A A. y e. A ( x [C.] y \/ x = y \/ y [C.] x ) )
12 df-so 
 |-  ( [C.] Or A <-> ( [C.] Po A /\ A. x e. A A. y e. A ( x [C.] y \/ x = y \/ y [C.] x ) ) )
13 2 11 12 3bitr4ri 
 |-  ( [C.] Or A <-> A. x e. A A. y e. A ( x C_ y \/ y C_ x ) )