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