Metamath Proof Explorer

Theorem porpss

Description: Every class is partially ordered by proper subsets. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion porpss 
|- [C.] Po A

Proof

Step Hyp Ref Expression
1 pssirr 
 |-  -. x C. x
2 psstr 
 |-  ( ( x C. y /\ y C. z ) -> x C. z )
3 vex 
 |-  x e. _V
4 3 brrpss 
 |-  ( x [C.] x <-> x C. x )
5 4 notbii 
 |-  ( -. x [C.] x <-> -. x C. x )
6 vex 
 |-  y e. _V
7 6 brrpss 
 |-  ( x [C.] y <-> x C. y )
8 vex 
 |-  z e. _V
9 8 brrpss 
 |-  ( y [C.] z <-> y C. z )
10 7 9 anbi12i 
 |-  ( ( x [C.] y /\ y [C.] z ) <-> ( x C. y /\ y C. z ) )
11 8 brrpss 
 |-  ( x [C.] z <-> x C. z )
12 10 11 imbi12i 
 |-  ( ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) <-> ( ( x C. y /\ y C. z ) -> x C. z ) )
13 5 12 anbi12i 
 |-  ( ( -. x [C.] x /\ ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) ) <-> ( -. x C. x /\ ( ( x C. y /\ y C. z ) -> x C. z ) ) )
14 1 2 13 mpbir2an 
 |-  ( -. x [C.] x /\ ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) )
15 14 rgenw 
 |-  A. z e. A ( -. x [C.] x /\ ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) )
16 15 rgen2w 
 |-  A. x e. A A. y e. A A. z e. A ( -. x [C.] x /\ ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) )
17 df-po 
 |-  ( [C.] Po A <-> A. x e. A A. y e. A A. z e. A ( -. x [C.] x /\ ( ( x [C.] y /\ y [C.] z ) -> x [C.] z ) ) )
18 16 17 mpbir 
 |-  [C.] Po A