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 ) )