Metamath Proof Explorer

Theorem sorpssi

Description: Property of a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion sorpssi ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B ⊆ C ∨ C ⊆ B

Proof

Step Hyp Ref Expression
1 solin ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B [⊂] C ∨ B = C ∨ C [⊂] B
2 elex ⊢ C ∈ A → C ∈ V
3 2 ad2antll ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → C ∈ V
4 brrpssg ⊢ C ∈ V → B [⊂] C ↔ B ⊂ C
5 3 4 syl ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B [⊂] C ↔ B ⊂ C
6 biidd ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B = C ↔ B = C
7 elex ⊢ B ∈ A → B ∈ V
8 7 ad2antrl ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B ∈ V
9 brrpssg ⊢ B ∈ V → C [⊂] B ↔ C ⊂ B
10 8 9 syl ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → C [⊂] B ↔ C ⊂ B
11 5 6 10 3orbi123d ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B [⊂] C ∨ B = C ∨ C [⊂] B ↔ B ⊂ C ∨ B = C ∨ C ⊂ B
12 1 11 mpbid ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B ⊂ C ∨ B = C ∨ C ⊂ B
13 sspsstri ⊢ B ⊆ C ∨ C ⊆ B ↔ B ⊂ C ∨ B = C ∨ C ⊂ B
14 12 13 sylibr ⊢ [⊂] Or A ∧ B ∈ A ∧ C ∈ A → B ⊆ C ∨ C ⊆ B