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

Metamath Proof Explorer

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 )