Metamath Proof Explorer

Theorem sspsstri

Description: Two ways of stating trichotomy with respect to inclusion. (Contributed by NM, 12-Aug-2004)

Ref Expression
Assertion sspsstri ⊢ A ⊆ B ∨ B ⊆ A ↔ A ⊂ B ∨ A = B ∨ B ⊂ A

Proof

Step Hyp Ref Expression
1 or32 ⊢ A ⊂ B ∨ B ⊂ A ∨ A = B ↔ A ⊂ B ∨ A = B ∨ B ⊂ A
2 sspss ⊢ A ⊆ B ↔ A ⊂ B ∨ A = B
3 sspss ⊢ B ⊆ A ↔ B ⊂ A ∨ B = A
4 eqcom ⊢ B = A ↔ A = B
5 4 orbi2i ⊢ B ⊂ A ∨ B = A ↔ B ⊂ A ∨ A = B
6 3 5 bitri ⊢ B ⊆ A ↔ B ⊂ A ∨ A = B
7 2 6 orbi12i ⊢ A ⊆ B ∨ B ⊆ A ↔ A ⊂ B ∨ A = B ∨ B ⊂ A ∨ A = B
8 orordir ⊢ A ⊂ B ∨ B ⊂ A ∨ A = B ↔ A ⊂ B ∨ A = B ∨ B ⊂ A ∨ A = B
9 7 8 bitr4i ⊢ A ⊆ B ∨ B ⊆ A ↔ A ⊂ B ∨ B ⊂ A ∨ A = B
10 df-3or ⊢ A ⊂ B ∨ A = B ∨ B ⊂ A ↔ A ⊂ B ∨ A = B ∨ B ⊂ A
11 1 9 10 3bitr4i ⊢ A ⊆ B ∨ B ⊆ A ↔ A ⊂ B ∨ A = B ∨ B ⊂ A