Proof of Theorem sstp
Step | Hyp | Ref
| Expression |
1 | | df-tp 4566 |
. . 3
⊢ {𝐵, 𝐶, 𝐷} = ({𝐵, 𝐶} ∪ {𝐷}) |
2 | 1 | sseq2i 3950 |
. 2
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})) |
3 | | 0ss 4330 |
. . 3
⊢ ∅
⊆ 𝐴 |
4 | 3 | biantrur 531 |
. 2
⊢ (𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷}) ↔ (∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷}))) |
5 | | ssunsn2 4760 |
. . 3
⊢ ((∅
⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})) ↔ ((∅ ⊆ 𝐴 ∧ 𝐴 ⊆ {𝐵, 𝐶}) ∨ ((∅ ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})))) |
6 | 3 | biantrur 531 |
. . . . 5
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ (∅ ⊆ 𝐴 ∧ 𝐴 ⊆ {𝐵, 𝐶})) |
7 | | sspr 4766 |
. . . . 5
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶}))) |
8 | 6, 7 | bitr3i 276 |
. . . 4
⊢ ((∅
⊆ 𝐴 ∧ 𝐴 ⊆ {𝐵, 𝐶}) ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶}))) |
9 | | uncom 4087 |
. . . . . . . 8
⊢ (∅
∪ {𝐷}) = ({𝐷} ∪
∅) |
10 | | un0 4324 |
. . . . . . . 8
⊢ ({𝐷} ∪ ∅) = {𝐷} |
11 | 9, 10 | eqtri 2766 |
. . . . . . 7
⊢ (∅
∪ {𝐷}) = {𝐷} |
12 | 11 | sseq1i 3949 |
. . . . . 6
⊢ ((∅
∪ {𝐷}) ⊆ 𝐴 ↔ {𝐷} ⊆ 𝐴) |
13 | | uncom 4087 |
. . . . . . 7
⊢ ({𝐵, 𝐶} ∪ {𝐷}) = ({𝐷} ∪ {𝐵, 𝐶}) |
14 | 13 | sseq2i 3950 |
. . . . . 6
⊢ (𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷}) ↔ 𝐴 ⊆ ({𝐷} ∪ {𝐵, 𝐶})) |
15 | 12, 14 | anbi12i 627 |
. . . . 5
⊢
(((∅ ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})) ↔ ({𝐷} ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐷} ∪ {𝐵, 𝐶}))) |
16 | | ssunpr 4765 |
. . . . 5
⊢ (({𝐷} ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐷} ∪ {𝐵, 𝐶})) ↔ ((𝐴 = {𝐷} ∨ 𝐴 = ({𝐷} ∪ {𝐵})) ∨ (𝐴 = ({𝐷} ∪ {𝐶}) ∨ 𝐴 = ({𝐷} ∪ {𝐵, 𝐶})))) |
17 | | uncom 4087 |
. . . . . . . . 9
⊢ ({𝐷} ∪ {𝐵}) = ({𝐵} ∪ {𝐷}) |
18 | | df-pr 4564 |
. . . . . . . . 9
⊢ {𝐵, 𝐷} = ({𝐵} ∪ {𝐷}) |
19 | 17, 18 | eqtr4i 2769 |
. . . . . . . 8
⊢ ({𝐷} ∪ {𝐵}) = {𝐵, 𝐷} |
20 | 19 | eqeq2i 2751 |
. . . . . . 7
⊢ (𝐴 = ({𝐷} ∪ {𝐵}) ↔ 𝐴 = {𝐵, 𝐷}) |
21 | 20 | orbi2i 910 |
. . . . . 6
⊢ ((𝐴 = {𝐷} ∨ 𝐴 = ({𝐷} ∪ {𝐵})) ↔ (𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷})) |
22 | | uncom 4087 |
. . . . . . . . 9
⊢ ({𝐷} ∪ {𝐶}) = ({𝐶} ∪ {𝐷}) |
23 | | df-pr 4564 |
. . . . . . . . 9
⊢ {𝐶, 𝐷} = ({𝐶} ∪ {𝐷}) |
24 | 22, 23 | eqtr4i 2769 |
. . . . . . . 8
⊢ ({𝐷} ∪ {𝐶}) = {𝐶, 𝐷} |
25 | 24 | eqeq2i 2751 |
. . . . . . 7
⊢ (𝐴 = ({𝐷} ∪ {𝐶}) ↔ 𝐴 = {𝐶, 𝐷}) |
26 | 1, 13 | eqtr2i 2767 |
. . . . . . . 8
⊢ ({𝐷} ∪ {𝐵, 𝐶}) = {𝐵, 𝐶, 𝐷} |
27 | 26 | eqeq2i 2751 |
. . . . . . 7
⊢ (𝐴 = ({𝐷} ∪ {𝐵, 𝐶}) ↔ 𝐴 = {𝐵, 𝐶, 𝐷}) |
28 | 25, 27 | orbi12i 912 |
. . . . . 6
⊢ ((𝐴 = ({𝐷} ∪ {𝐶}) ∨ 𝐴 = ({𝐷} ∪ {𝐵, 𝐶})) ↔ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})) |
29 | 21, 28 | orbi12i 912 |
. . . . 5
⊢ (((𝐴 = {𝐷} ∨ 𝐴 = ({𝐷} ∪ {𝐵})) ∨ (𝐴 = ({𝐷} ∪ {𝐶}) ∨ 𝐴 = ({𝐷} ∪ {𝐵, 𝐶}))) ↔ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}))) |
30 | 15, 16, 29 | 3bitri 297 |
. . . 4
⊢
(((∅ ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})) ↔ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}))) |
31 | 8, 30 | orbi12i 912 |
. . 3
⊢
(((∅ ⊆ 𝐴
∧ 𝐴 ⊆ {𝐵, 𝐶}) ∨ ((∅ ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷}))) ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})))) |
32 | 5, 31 | bitri 274 |
. 2
⊢ ((∅
⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})) ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})))) |
33 | 2, 4, 32 | 3bitri 297 |
1
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})))) |