Metamath Proof Explorer


Theorem sorpssi

Description: Property of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion sorpssi
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C_ C \/ C C_ B ) )

Proof

Step Hyp Ref Expression
1 solin
 |-  ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B [C.] C \/ B = C \/ C [C.] B ) )
2 elex
 |-  ( C e. A -> C e. _V )
3 2 ad2antll
 |-  ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> C e. _V )
4 brrpssg
 |-  ( C e. _V -> ( B [C.] C <-> B C. C ) )
5 3 4 syl
 |-  ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B [C.] C <-> B C. C ) )
6 biidd
 |-  ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C <-> B = C ) )
7 elex
 |-  ( B e. A -> B e. _V )
8 7 ad2antrl
 |-  ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> B e. _V )
9 brrpssg
 |-  ( B e. _V -> ( C [C.] B <-> C C. B ) )
10 8 9 syl
 |-  ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( C [C.] B <-> C C. B ) )
11 5 6 10 3orbi123d
 |-  ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( ( B [C.] C \/ B = C \/ C [C.] B ) <-> ( B C. C \/ B = C \/ C C. B ) ) )
12 1 11 mpbid
 |-  ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C. C \/ B = C \/ C C. B ) )
13 sspsstri
 |-  ( ( B C_ C \/ C C_ B ) <-> ( B C. C \/ B = C \/ C C. B ) )
14 12 13 sylibr
 |-  ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C_ C \/ C C_ B ) )