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

Metamath Proof Explorer

Theorem ssunpr

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 ssunpr ⊢ B ⊆ A ∧ A ⊆ B ∪ C D ↔ A = B ∨ A = B ∪ C ∨ A = B ∪ D ∨ A = B ∪ C D

Proof

Step Hyp Ref Expression
1 df-pr ⊢ C D = C ∪ D
2 1 uneq2i ⊢ B ∪ C D = B ∪ C ∪ D
3 unass ⊢ B ∪ C ∪ D = B ∪ C ∪ D
4 2 3 eqtr4i ⊢ B ∪ C D = B ∪ C ∪ D
5 4 sseq2i ⊢ A ⊆ B ∪ C D ↔ A ⊆ B ∪ C ∪ D
6 5 anbi2i ⊢ B ⊆ A ∧ A ⊆ B ∪ C D ↔ B ⊆ A ∧ A ⊆ B ∪ C ∪ D
7 ssunsn2 ⊢ B ⊆ A ∧ A ⊆ B ∪ C ∪ D ↔ B ⊆ A ∧ A ⊆ B ∪ C ∨ B ∪ D ⊆ A ∧ A ⊆ B ∪ C ∪ D
8 ssunsn ⊢ B ⊆ A ∧ A ⊆ B ∪ C ↔ A = B ∨ A = B ∪ C
9 un23 ⊢ B ∪ C ∪ D = B ∪ D ∪ C
10 9 sseq2i ⊢ A ⊆ B ∪ C ∪ D ↔ A ⊆ B ∪ D ∪ C
11 10 anbi2i ⊢ B ∪ D ⊆ A ∧ A ⊆ B ∪ C ∪ D ↔ B ∪ D ⊆ A ∧ A ⊆ B ∪ D ∪ C
12 ssunsn ⊢ B ∪ D ⊆ A ∧ A ⊆ B ∪ D ∪ C ↔ A = B ∪ D ∨ A = B ∪ D ∪ C
13 4 9 eqtr2i ⊢ B ∪ D ∪ C = B ∪ C D
14 13 eqeq2i ⊢ A = B ∪ D ∪ C ↔ A = B ∪ C D
15 14 orbi2i ⊢ A = B ∪ D ∨ A = B ∪ D ∪ C ↔ A = B ∪ D ∨ A = B ∪ C D
16 11 12 15 3bitri ⊢ B ∪ D ⊆ A ∧ A ⊆ B ∪ C ∪ D ↔ A = B ∪ D ∨ A = B ∪ C D
17 8 16 orbi12i ⊢ B ⊆ A ∧ A ⊆ B ∪ C ∨ B ∪ D ⊆ A ∧ A ⊆ B ∪ C ∪ D ↔ A = B ∨ A = B ∪ C ∨ A = B ∪ D ∨ A = B ∪ C D
18 6 7 17 3bitri ⊢ B ⊆ A ∧ A ⊆ B ∪ C D ↔ A = B ∨ A = B ∪ C ∨ A = B ∪ D ∨ A = B ∪ C D