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 ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 or32 ⊢ ( ( ( 𝐴 ⊊ 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ∨ 𝐴 = 𝐵 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ 𝐵 ⊊ 𝐴 ) )
2 sspss ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) )
3 sspss ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) )
4 eqcom ⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
5 4 orbi2i ⊢ ( ( 𝐵 ⊊ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ( 𝐵 ⊊ 𝐴 ∨ 𝐴 = 𝐵 ) )
6 3 5 bitri ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ⊊ 𝐴 ∨ 𝐴 = 𝐵 ) )
7 2 6 orbi12i ⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ ( 𝐵 ⊊ 𝐴 ∨ 𝐴 = 𝐵 ) ) )
8 orordir ⊢ ( ( ( 𝐴 ⊊ 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ∨ 𝐴 = 𝐵 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ ( 𝐵 ⊊ 𝐴 ∨ 𝐴 = 𝐵 ) ) )
9 7 8 bitr4i ⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ∨ 𝐴 = 𝐵 ) )
10 df-3or ⊢ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴 ) ↔ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ∨ 𝐵 ⊊ 𝐴 ) )
11 1 9 10 3bitr4i ⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴 ) )