This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ∩ 𝐶 ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → 𝐵 ∈ 𝐴 )
2 dfss2 ⊢ ( 𝐵 ⊆ 𝐶 ↔ ( 𝐵 ∩ 𝐶 ) = 𝐵 )
3 eleq1 ⊢ ( ( 𝐵 ∩ 𝐶 ) = 𝐵 → ( ( 𝐵 ∩ 𝐶 ) ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
4 2 3 sylbi ⊢ ( 𝐵 ⊆ 𝐶 → ( ( 𝐵 ∩ 𝐶 ) ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
5 1 4 syl5ibrcom ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ⊆ 𝐶 → ( 𝐵 ∩ 𝐶 ) ∈ 𝐴 ) )
6 simprr ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → 𝐶 ∈ 𝐴 )
7 sseqin2 ⊢ ( 𝐶 ⊆ 𝐵 ↔ ( 𝐵 ∩ 𝐶 ) = 𝐶 )
8 eleq1 ⊢ ( ( 𝐵 ∩ 𝐶 ) = 𝐶 → ( ( 𝐵 ∩ 𝐶 ) ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
9 7 8 sylbi ⊢ ( 𝐶 ⊆ 𝐵 → ( ( 𝐵 ∩ 𝐶 ) ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
10 6 9 syl5ibrcom ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐶 ⊆ 𝐵 → ( 𝐵 ∩ 𝐶 ) ∈ 𝐴 ) )
11 sorpssi ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) )
12 5 10 11 mpjaod ⊢ ( ( [⊊] Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ( 𝐵 ∩ 𝐶 ) ∈ 𝐴 )