Theorem sorpssin

Description: A chain of sets is closed under binary intersection. (Contributed by Mario Carneiro, 16-May-2015)

	Ref	Expression
Assertion	sorpssin	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B i^i C ) e. A )

Proof

Step	Hyp	Ref	Expression
1		simprl	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> B e. A )
2		dfss2	|- ( B C_ C <-> ( B i^i C ) = B )
3		eleq1	|- ( ( B i^i C ) = B -> ( ( B i^i C ) e. A <-> B e. A ) )
4	2 3	sylbi	|- ( B C_ C -> ( ( B i^i C ) e. A <-> B e. A ) )
5	1 4	syl5ibrcom	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C_ C -> ( B i^i C ) e. A ) )
6		simprr	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> C e. A )
7		sseqin2	|- ( C C_ B <-> ( B i^i C ) = C )
8		eleq1	|- ( ( B i^i C ) = C -> ( ( B i^i C ) e. A <-> C e. A ) )
9	7 8	sylbi	|- ( C C_ B -> ( ( B i^i C ) e. A <-> C e. A ) )
10	6 9	syl5ibrcom	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( C C_ B -> ( B i^i C ) e. A ) )
11		sorpssi	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C_ C \/ C C_ B ) )
12	5 10 11	mpjaod	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B i^i C ) e. A )