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	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 } ) ) )