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 [⊂] Or A B A C A B C A

Proof

Step Hyp Ref Expression
1 simprr [⊂] Or A B A C A C A
2 ssequn1 B C B C = C
3 eleq1 B C = C B C A C A
4 2 3 sylbi B C B C A C A
5 1 4 syl5ibrcom [⊂] Or A B A C A B C B C A
6 simprl [⊂] Or A B A C A B A
7 ssequn2 C B B C = B
8 eleq1 B C = B B C A B A
9 7 8 sylbi C B B C A B A
10 6 9 syl5ibrcom [⊂] Or A B A C A C B B C A
11 sorpssi [⊂] Or A B A C A B C C B
12 5 10 11 mpjaod [⊂] Or A B A C A B C A