Theorem sorpssun

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

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

Proof

Step	Hyp	Ref	Expression
1		simprr	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> C e. A )
2		ssequn1	|- ( B C_ C <-> ( B u. C ) = C )
3		eleq1	|- ( ( B u. C ) = C -> ( ( B u. C ) e. A <-> C e. A ) )
4	2 3	sylbi	|- ( B C_ C -> ( ( B u. C ) e. A <-> C e. A ) )
5	1 4	syl5ibrcom	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C_ C -> ( B u. C ) e. A ) )
6		simprl	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> B e. A )
7		ssequn2	|- ( C C_ B <-> ( B u. C ) = B )
8		eleq1	|- ( ( B u. C ) = B -> ( ( B u. C ) e. A <-> B e. A ) )
9	7 8	sylbi	|- ( C C_ B -> ( ( B u. C ) e. A <-> B e. A ) )
10	6 9	syl5ibrcom	|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( C C_ B -> ( B u. 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 u. C ) e. A )