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

Proof

Step Hyp Ref Expression
1 simprl ⊢[⊂]OrA∧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 ⊢[⊂]OrA∧B∈A∧C∈A→B⊆C→B∩C∈A
6 simprr ⊢[⊂]OrA∧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 ⊢[⊂]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