Proof of Theorem sstp
Step | Hyp | Ref
| Expression |
1 | | df-tp 4521 |
. . 3
⊢ {𝐵, 𝐶, 𝐷} = ({𝐵, 𝐶} ∪ {𝐷}) |
2 | 1 | sseq2i 3906 |
. 2
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})) |
3 | | 0ss 4285 |
. . 3
⊢ ∅
⊆ 𝐴 |
4 | 3 | biantrur 534 |
. 2
⊢ (𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷}) ↔ (∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷}))) |
5 | | ssunsn2 4715 |
. . 3
⊢ ((∅
⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})) ↔ ((∅ ⊆ 𝐴 ∧ 𝐴 ⊆ {𝐵, 𝐶}) ∨ ((∅ ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})))) |
6 | 3 | biantrur 534 |
. . . . 5
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ (∅ ⊆ 𝐴 ∧ 𝐴 ⊆ {𝐵, 𝐶})) |
7 | | sspr 4721 |
. . . . 5
⊢ (𝐴 ⊆ {𝐵, 𝐶} ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶}))) |
8 | 6, 7 | bitr3i 280 |
. . . 4
⊢ ((∅
⊆ 𝐴 ∧ 𝐴 ⊆ {𝐵, 𝐶}) ↔ ((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶}))) |
9 | | uncom 4043 |
. . . . . . . 8
⊢ (∅
∪ {𝐷}) = ({𝐷} ∪
∅) |
10 | | un0 4279 |
. . . . . . . 8
⊢ ({𝐷} ∪ ∅) = {𝐷} |
11 | 9, 10 | eqtri 2761 |
. . . . . . 7
⊢ (∅
∪ {𝐷}) = {𝐷} |
12 | 11 | sseq1i 3905 |
. . . . . 6
⊢ ((∅
∪ {𝐷}) ⊆ 𝐴 ↔ {𝐷} ⊆ 𝐴) |
13 | | uncom 4043 |
. . . . . . 7
⊢ ({𝐵, 𝐶} ∪ {𝐷}) = ({𝐷} ∪ {𝐵, 𝐶}) |
14 | 13 | sseq2i 3906 |
. . . . . 6
⊢ (𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷}) ↔ 𝐴 ⊆ ({𝐷} ∪ {𝐵, 𝐶})) |
15 | 12, 14 | anbi12i 630 |
. . . . 5
⊢
(((∅ ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})) ↔ ({𝐷} ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐷} ∪ {𝐵, 𝐶}))) |
16 | | ssunpr 4720 |
. . . . 5
⊢ (({𝐷} ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐷} ∪ {𝐵, 𝐶})) ↔ ((𝐴 = {𝐷} ∨ 𝐴 = ({𝐷} ∪ {𝐵})) ∨ (𝐴 = ({𝐷} ∪ {𝐶}) ∨ 𝐴 = ({𝐷} ∪ {𝐵, 𝐶})))) |
17 | | uncom 4043 |
. . . . . . . . 9
⊢ ({𝐷} ∪ {𝐵}) = ({𝐵} ∪ {𝐷}) |
18 | | df-pr 4519 |
. . . . . . . . 9
⊢ {𝐵, 𝐷} = ({𝐵} ∪ {𝐷}) |
19 | 17, 18 | eqtr4i 2764 |
. . . . . . . 8
⊢ ({𝐷} ∪ {𝐵}) = {𝐵, 𝐷} |
20 | 19 | eqeq2i 2751 |
. . . . . . 7
⊢ (𝐴 = ({𝐷} ∪ {𝐵}) ↔ 𝐴 = {𝐵, 𝐷}) |
21 | 20 | orbi2i 912 |
. . . . . 6
⊢ ((𝐴 = {𝐷} ∨ 𝐴 = ({𝐷} ∪ {𝐵})) ↔ (𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷})) |
22 | | uncom 4043 |
. . . . . . . . 9
⊢ ({𝐷} ∪ {𝐶}) = ({𝐶} ∪ {𝐷}) |
23 | | df-pr 4519 |
. . . . . . . . 9
⊢ {𝐶, 𝐷} = ({𝐶} ∪ {𝐷}) |
24 | 22, 23 | eqtr4i 2764 |
. . . . . . . 8
⊢ ({𝐷} ∪ {𝐶}) = {𝐶, 𝐷} |
25 | 24 | eqeq2i 2751 |
. . . . . . 7
⊢ (𝐴 = ({𝐷} ∪ {𝐶}) ↔ 𝐴 = {𝐶, 𝐷}) |
26 | 1, 13 | eqtr2i 2762 |
. . . . . . . 8
⊢ ({𝐷} ∪ {𝐵, 𝐶}) = {𝐵, 𝐶, 𝐷} |
27 | 26 | eqeq2i 2751 |
. . . . . . 7
⊢ (𝐴 = ({𝐷} ∪ {𝐵, 𝐶}) ↔ 𝐴 = {𝐵, 𝐶, 𝐷}) |
28 | 25, 27 | orbi12i 914 |
. . . . . 6
⊢ ((𝐴 = ({𝐷} ∪ {𝐶}) ∨ 𝐴 = ({𝐷} ∪ {𝐵, 𝐶})) ↔ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})) |
29 | 21, 28 | orbi12i 914 |
. . . . 5
⊢ (((𝐴 = {𝐷} ∨ 𝐴 = ({𝐷} ∪ {𝐵})) ∨ (𝐴 = ({𝐷} ∪ {𝐶}) ∨ 𝐴 = ({𝐷} ∪ {𝐵, 𝐶}))) ↔ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}))) |
30 | 15, 16, 29 | 3bitri 300 |
. . . 4
⊢
(((∅ ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})) ↔ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷}))) |
31 | 8, 30 | orbi12i 914 |
. . 3
⊢
(((∅ ⊆ 𝐴
∧ 𝐴 ⊆ {𝐵, 𝐶}) ∨ ((∅ ∪ {𝐷}) ⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷}))) ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})))) |
32 | 5, 31 | bitri 278 |
. 2
⊢ ((∅
⊆ 𝐴 ∧ 𝐴 ⊆ ({𝐵, 𝐶} ∪ {𝐷})) ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})))) |
33 | 2, 4, 32 | 3bitri 300 |
1
⊢ (𝐴 ⊆ {𝐵, 𝐶, 𝐷} ↔ (((𝐴 = ∅ ∨ 𝐴 = {𝐵}) ∨ (𝐴 = {𝐶} ∨ 𝐴 = {𝐵, 𝐶})) ∨ ((𝐴 = {𝐷} ∨ 𝐴 = {𝐵, 𝐷}) ∨ (𝐴 = {𝐶, 𝐷} ∨ 𝐴 = {𝐵, 𝐶, 𝐷})))) |