Metamath Proof Explorer

Theorem sorpssin

Description: A chain of sets is closed under binary intersection. (Contributed by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion sorpssin ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B ∩ C ∈ A

Proof

Step Hyp Ref Expression
1 simprl ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B ∈ A
2 df-ss ⊢ B ⊆ C ↔ B ∩ C = B
3 eleq1 ⊢ B ∩ C = B → B ∩ C ∈ A ↔ B ∈ A
4 2 3 sylbi ⊢ B ⊆ C → B ∩ C ∈ A ↔ B ∈ A
5 1 4 syl5ibrcom ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B ⊆ C → B ∩ C ∈ A
6 simprr ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → C ∈ A
7 sseqin2 ⊢ C ⊆ B ↔ B ∩ C = C
8 eleq1 ⊢ B ∩ C = C → B ∩ C ∈ A ↔ C ∈ A
9 7 8 sylbi ⊢ C ⊆ B → B ∩ C ∈ A ↔ C ∈ 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