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

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

Proof

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