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

Metamath Proof Explorer

Theorem sspr

Description: The subsets of a pair. (Contributed by NM, 16-Mar-2006) (Proof shortened by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion sspr ⊢ A ⊆ B C ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C

Proof

Step Hyp Ref Expression
1 uncom ⊢ ∅ ∪ B C = B C ∪ ∅
2 un0 ⊢ B C ∪ ∅ = B C
3 1 2 eqtri ⊢ ∅ ∪ B C = B C
4 3 sseq2i ⊢ A ⊆ ∅ ∪ B C ↔ A ⊆ B C
5 0ss ⊢ ∅ ⊆ A
6 5 biantrur ⊢ A ⊆ ∅ ∪ B C ↔ ∅ ⊆ A ∧ A ⊆ ∅ ∪ B C
7 4 6 bitr3i ⊢ A ⊆ B C ↔ ∅ ⊆ A ∧ A ⊆ ∅ ∪ B C
8 ssunpr ⊢ ∅ ⊆ A ∧ A ⊆ ∅ ∪ B C ↔ A = ∅ ∨ A = ∅ ∪ B ∨ A = ∅ ∪ C ∨ A = ∅ ∪ B C
9 uncom ⊢ ∅ ∪ B = B ∪ ∅
10 un0 ⊢ B ∪ ∅ = B
11 9 10 eqtri ⊢ ∅ ∪ B = B
12 11 eqeq2i ⊢ A = ∅ ∪ B ↔ A = B
13 12 orbi2i ⊢ A = ∅ ∨ A = ∅ ∪ B ↔ A = ∅ ∨ A = B
14 uncom ⊢ ∅ ∪ C = C ∪ ∅
15 un0 ⊢ C ∪ ∅ = C
16 14 15 eqtri ⊢ ∅ ∪ C = C
17 16 eqeq2i ⊢ A = ∅ ∪ C ↔ A = C
18 3 eqeq2i ⊢ A = ∅ ∪ B C ↔ A = B C
19 17 18 orbi12i ⊢ A = ∅ ∪ C ∨ A = ∅ ∪ B C ↔ A = C ∨ A = B C
20 13 19 orbi12i ⊢ A = ∅ ∨ A = ∅ ∪ B ∨ A = ∅ ∪ C ∨ A = ∅ ∪ B C ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C
21 7 8 20 3bitri ⊢ A ⊆ B C ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C