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