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 C_ B \/ B C_ A ) <-> ( A C. B \/ A = B \/ B C. A ) )

Proof

Step Hyp Ref Expression
1 or32
 |-  ( ( ( A C. B \/ B C. A ) \/ A = B ) <-> ( ( A C. B \/ A = B ) \/ B C. A ) )
2 sspss
 |-  ( A C_ B <-> ( A C. B \/ A = B ) )
3 sspss
 |-  ( B C_ A <-> ( B C. A \/ B = A ) )
4 eqcom
 |-  ( B = A <-> A = B )
5 4 orbi2i
 |-  ( ( B C. A \/ B = A ) <-> ( B C. A \/ A = B ) )
6 3 5 bitri
 |-  ( B C_ A <-> ( B C. A \/ A = B ) )
7 2 6 orbi12i
 |-  ( ( A C_ B \/ B C_ A ) <-> ( ( A C. B \/ A = B ) \/ ( B C. A \/ A = B ) ) )
8 orordir
 |-  ( ( ( A C. B \/ B C. A ) \/ A = B ) <-> ( ( A C. B \/ A = B ) \/ ( B C. A \/ A = B ) ) )
9 7 8 bitr4i
 |-  ( ( A C_ B \/ B C_ A ) <-> ( ( A C. B \/ B C. A ) \/ A = B ) )
10 df-3or
 |-  ( ( A C. B \/ A = B \/ B C. A ) <-> ( ( A C. B \/ A = B ) \/ B C. A ) )
11 1 9 10 3bitr4i
 |-  ( ( A C_ B \/ B C_ A ) <-> ( A C. B \/ A = B \/ B C. A ) )