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

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 ) )