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 df-ss ( 𝐵𝐶 ↔ ( 𝐵𝐶 ) = 𝐵 )
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 𝐴 ∧ ( 𝐵𝐴𝐶𝐴 ) ) → ( 𝐵𝐶 ) ∈ 𝐴 )