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 ⊢[⊂]OrA∧B∈A∧C∈A→B∪C∈A

Proof

Step Hyp Ref Expression
1 simprr ⊢[⊂]OrA∧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 ⊢[⊂]OrA∧B∈A∧C∈A→B⊆C→B∪C∈A
6 simprl ⊢[⊂]OrA∧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 ⊢[⊂]OrA∧B∈A∧C∈A→C⊆B→B∪C∈A
11 sorpssi ⊢[⊂]OrA∧B∈A∧C∈A→B⊆C∨C⊆B
12 5 10 11 mpjaod ⊢[⊂]OrA∧B∈A∧C∈A→B∪C∈A