Metamath Proof Explorer

Theorem sstp

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

Ref Expression
Assertion sstp ⊢A⊆BCD↔A=∅∨A=B∨A=C∨A=BC∨A=D∨A=BD∨A=CD∨A=BCD

Proof

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