Metamath Proof Explorer

Theorem sorpssi

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

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

Proof

Step Hyp Ref Expression
1 solin ⊢[⊂]OrA∧B∈A∧C∈A→B[⊂]C∨B=C∨C[⊂]B
2 elex ⊢C∈A→C∈V
3 2 ad2antll ⊢[⊂]OrA∧B∈A∧C∈A→C∈V
4 brrpssg ⊢C∈V→B[⊂]C↔B⊂C
5 3 4 syl ⊢[⊂]OrA∧B∈A∧C∈A→B[⊂]C↔B⊂C
6 biidd ⊢[⊂]OrA∧B∈A∧C∈A→B=C↔B=C
7 elex ⊢B∈A→B∈V
8 7 ad2antrl ⊢[⊂]OrA∧B∈A∧C∈A→B∈V
9 brrpssg ⊢B∈V→C[⊂]B↔C⊂B
10 8 9 syl ⊢[⊂]OrA∧B∈A∧C∈A→C[⊂]B↔C⊂B
11 5 6 10 3orbi123d ⊢[⊂]OrA∧B∈A∧C∈A→B[⊂]C∨B=C∨C[⊂]B↔B⊂C∨B=C∨C⊂B
12 1 11 mpbid ⊢[⊂]OrA∧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 ⊢[⊂]OrA∧B∈A∧C∈A→B⊆C∨C⊆B