This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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