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 0un ⊢ ∅ ∪ D = D
10 9 sseq1i ⊢ ∅ ∪ D ⊆ A ↔ D ⊆ A
11 uncom ⊢ B C ∪ D = D ∪ B C
12 11 sseq2i ⊢ A ⊆ B C ∪ D ↔ A ⊆ D ∪ B C
13 10 12 anbi12i ⊢ ∅ ∪ D ⊆ A ∧ A ⊆ B C ∪ D ↔ D ⊆ A ∧ A ⊆ D ∪ B C
14 ssunpr ⊢ D ⊆ A ∧ A ⊆ D ∪ B C ↔ A = D ∨ A = D ∪ B ∨ A = D ∪ C ∨ A = D ∪ B C
15 uncom ⊢ D ∪ B = B ∪ D
16 df-pr ⊢ B D = B ∪ D
17 15 16 eqtr4i ⊢ D ∪ B = B D
18 17 eqeq2i ⊢ A = D ∪ B ↔ A = B D
19 18 orbi2i ⊢ A = D ∨ A = D ∪ B ↔ A = D ∨ A = B D
20 uncom ⊢ D ∪ C = C ∪ D
21 df-pr ⊢ C D = C ∪ D
22 20 21 eqtr4i ⊢ D ∪ C = C D
23 22 eqeq2i ⊢ A = D ∪ C ↔ A = C D
24 1 11 eqtr2i ⊢ D ∪ B C = B C D
25 24 eqeq2i ⊢ A = D ∪ B C ↔ A = B C D
26 23 25 orbi12i ⊢ A = D ∪ C ∨ A = D ∪ B C ↔ A = C D ∨ A = B C D
27 19 26 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
28 13 14 27 3bitri ⊢ ∅ ∪ D ⊆ A ∧ A ⊆ B C ∪ D ↔ A = D ∨ A = B D ∨ A = C D ∨ A = B C D
29 8 28 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
30 5 29 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
31 2 4 30 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