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

Metamath Proof Explorer

Theorem ssunsn

Description: Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion ssunsn ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 } ) ) )

Proof

Step Hyp Ref Expression
1 ssunsn2 ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∨ ( ( 𝐵 ∪ { 𝐶 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ) )
2 ancom ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
3 eqss ⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
4 2 3 bitr4i ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ↔ 𝐴 = 𝐵 )
5 ancom ⊢ ( ( ( 𝐵 ∪ { 𝐶 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ↔ ( 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ∧ ( 𝐵 ∪ { 𝐶 } ) ⊆ 𝐴 ) )
6 eqss ⊢ ( 𝐴 = ( 𝐵 ∪ { 𝐶 } ) ↔ ( 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ∧ ( 𝐵 ∪ { 𝐶 } ) ⊆ 𝐴 ) )
7 5 6 bitr4i ⊢ ( ( ( 𝐵 ∪ { 𝐶 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ↔ 𝐴 = ( 𝐵 ∪ { 𝐶 } ) )
8 4 7 orbi12i ⊢ ( ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵 ) ∨ ( ( 𝐵 ∪ { 𝐶 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 } ) ) )
9 1 8 bitri ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 } ) ) )