Metamath Proof Explorer

Theorem sstp

Description: The subsets of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016)

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

Proof

Step Hyp Ref Expression
1 df-tp ⊢ B C D = B C ∪ D
2 1 sseq2i ⊢ A ⊆ B C D ↔ A ⊆ B C ∪ D
3 0ss ⊢ ∅ ⊆ A
4 3 biantrur ⊢ A ⊆ B C ∪ D ↔ ∅ ⊆ A ∧ A ⊆ B C ∪ D
5 ssunsn2 ⊢ ∅ ⊆ A ∧ A ⊆ B C ∪ D ↔ ∅ ⊆ A ∧ A ⊆ B C ∨ ∅ ∪ D ⊆ A ∧ A ⊆ B C ∪ D
6 3 biantrur ⊢ A ⊆ B C ↔ ∅ ⊆ A ∧ A ⊆ B C
7 sspr ⊢ A ⊆ B C ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C
8 6 7 bitr3i ⊢ ∅ ⊆ A ∧ A ⊆ B C ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C
9 uncom ⊢ ∅ ∪ D = D ∪ ∅
10 un0 ⊢ D ∪ ∅ = D
11 9 10 eqtri ⊢ ∅ ∪ D = D
12 11 sseq1i ⊢ ∅ ∪ D ⊆ A ↔ D ⊆ A
13 uncom ⊢ B C ∪ D = D ∪ B C
14 13 sseq2i ⊢ A ⊆ B C ∪ D ↔ A ⊆ D ∪ B C
15 12 14 anbi12i ⊢ ∅ ∪ D ⊆ A ∧ A ⊆ B C ∪ D ↔ D ⊆ A ∧ A ⊆ D ∪ B C
16 ssunpr ⊢ D ⊆ A ∧ A ⊆ D ∪ B C ↔ A = D ∨ A = D ∪ B ∨ A = D ∪ C ∨ A = D ∪ B C
17 uncom ⊢ D ∪ B = B ∪ D
18 df-pr ⊢ B D = B ∪ D
19 17 18 eqtr4i ⊢ D ∪ B = B D
20 19 eqeq2i ⊢ A = D ∪ B ↔ A = B D
21 20 orbi2i ⊢ A = D ∨ A = D ∪ B ↔ A = D ∨ A = B D
22 uncom ⊢ D ∪ C = C ∪ D
23 df-pr ⊢ C D = C ∪ D
24 22 23 eqtr4i ⊢ D ∪ C = C D
25 24 eqeq2i ⊢ A = D ∪ C ↔ A = C D
26 1 13 eqtr2i ⊢ D ∪ B C = B C D
27 26 eqeq2i ⊢ A = D ∪ B C ↔ A = B C D
28 25 27 orbi12i ⊢ A = D ∪ C ∨ A = D ∪ B C ↔ A = C D ∨ A = B C D
29 21 28 orbi12i ⊢ A = D ∨ A = D ∪ B ∨ A = D ∪ C ∨ A = D ∪ B C ↔ A = D ∨ A = B D ∨ A = C D ∨ A = B C D
30 15 16 29 3bitri ⊢ ∅ ∪ D ⊆ A ∧ A ⊆ B C ∪ D ↔ A = D ∨ A = B D ∨ A = C D ∨ A = B C D
31 8 30 orbi12i ⊢ ∅ ⊆ A ∧ A ⊆ B C ∨ ∅ ∪ D ⊆ A ∧ A ⊆ B C ∪ D ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C ∨ A = D ∨ A = B D ∨ A = C D ∨ A = B C D
32 5 31 bitri ⊢ ∅ ⊆ A ∧ A ⊆ B C ∪ D ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C ∨ A = D ∨ A = B D ∨ A = C D ∨ A = B C D
33 2 4 32 3bitri ⊢ A ⊆ B C D ↔ A = ∅ ∨ A = B ∨ A = C ∨ A = B C ∨ A = D ∨ A = B D ∨ A = C D ∨ A = B C D