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 )