Step | Hyp | Ref
| Expression |
1 | | sstpr 3519 |
. . 3
⊢
((((x = ∅ ∨ x = {A}) ∨ (x = {B} ∨ x = {A, B})) ∨ ((x = {𝐶}
∨ x = {A, 𝐶}) ∨
(x = {B, 𝐶} ∨
x = {A,
B, 𝐶}))) → x ⊆ {A,
B, 𝐶}) |
2 | | elun 3078 |
. . . 4
⊢ (x ∈ (({∅,
{A}} ∪ {{B}, {A, B}}) ∪ ({{𝐶}, {A,
𝐶}} ∪ {{B, 𝐶}, {A,
B, 𝐶}})) ↔ (x ∈ ({∅,
{A}} ∪ {{B}, {A, B}}) ∨ x ∈ ({{𝐶}, {A, 𝐶}} ∪ {{B, 𝐶}, {A,
B, 𝐶}}))) |
3 | | elun 3078 |
. . . . . 6
⊢ (x ∈ ({∅,
{A}} ∪ {{B}, {A, B}}) ↔ (x
∈ {∅, {A}} ∨ x ∈ {{B}, {A, B}})) |
4 | | vex 2554 |
. . . . . . . 8
⊢ x ∈
V |
5 | 4 | elpr 3385 |
. . . . . . 7
⊢ (x ∈ {∅,
{A}} ↔ (x = ∅ ∨
x = {A})) |
6 | 4 | elpr 3385 |
. . . . . . 7
⊢ (x ∈ {{B}, {A, B}} ↔ (x =
{B} ∨
x = {A,
B})) |
7 | 5, 6 | orbi12i 680 |
. . . . . 6
⊢
((x ∈ {∅, {A}} ∨ x ∈ {{B}, {A, B}}) ↔ ((x
= ∅ ∨ x = {A}) ∨ (x = {B} ∨ x = {A, B}))) |
8 | 3, 7 | bitri 173 |
. . . . 5
⊢ (x ∈ ({∅,
{A}} ∪ {{B}, {A, B}}) ↔ ((x
= ∅ ∨ x = {A}) ∨ (x = {B} ∨ x = {A, B}))) |
9 | | elun 3078 |
. . . . . 6
⊢ (x ∈ ({{𝐶}, {A, 𝐶}} ∪ {{B, 𝐶}, {A,
B, 𝐶}}) ↔ (x ∈ {{𝐶}, {A, 𝐶}} ∨
x ∈
{{B, 𝐶}, {A,
B, 𝐶}})) |
10 | 4 | elpr 3385 |
. . . . . . 7
⊢ (x ∈ {{𝐶}, {A, 𝐶}} ↔ (x = {𝐶} ∨
x = {A,
𝐶})) |
11 | 4 | elpr 3385 |
. . . . . . 7
⊢ (x ∈ {{B, 𝐶}, {A,
B, 𝐶}} ↔ (x = {B, 𝐶}
∨ x = {A, B, 𝐶})) |
12 | 10, 11 | orbi12i 680 |
. . . . . 6
⊢
((x ∈ {{𝐶}, {A,
𝐶}}
∨ x ∈ {{B, 𝐶}, {A, B, 𝐶}}) ↔ ((x = {𝐶} ∨
x = {A,
𝐶})
∨ (x = {B, 𝐶} ∨
x = {A,
B, 𝐶}))) |
13 | 9, 12 | bitri 173 |
. . . . 5
⊢ (x ∈ ({{𝐶}, {A, 𝐶}} ∪ {{B, 𝐶}, {A,
B, 𝐶}}) ↔ ((x = {𝐶} ∨
x = {A,
𝐶})
∨ (x = {B, 𝐶} ∨
x = {A,
B, 𝐶}))) |
14 | 8, 13 | orbi12i 680 |
. . . 4
⊢
((x ∈ ({∅, {A}} ∪ {{B},
{A, B}}) ∨ x ∈ ({{𝐶}, {A, 𝐶}} ∪ {{B, 𝐶}, {A,
B, 𝐶}})) ↔ (((x = ∅ ∨
x = {A}) ∨ (x = {B} ∨ x = {A, B})) ∨ ((x = {𝐶}
∨ x = {A, 𝐶}) ∨
(x = {B, 𝐶} ∨
x = {A,
B, 𝐶})))) |
15 | 2, 14 | bitri 173 |
. . 3
⊢ (x ∈ (({∅,
{A}} ∪ {{B}, {A, B}}) ∪ ({{𝐶}, {A,
𝐶}} ∪ {{B, 𝐶}, {A,
B, 𝐶}})) ↔ (((x = ∅ ∨
x = {A}) ∨ (x = {B} ∨ x = {A, B})) ∨ ((x = {𝐶}
∨ x = {A, 𝐶}) ∨
(x = {B, 𝐶} ∨
x = {A,
B, 𝐶})))) |
16 | 4 | elpw 3357 |
. . 3
⊢ (x ∈ 𝒫
{A, B,
𝐶} ↔ x ⊆ {A,
B, 𝐶}) |
17 | 1, 15, 16 | 3imtr4i 190 |
. 2
⊢ (x ∈ (({∅,
{A}} ∪ {{B}, {A, B}}) ∪ ({{𝐶}, {A,
𝐶}} ∪ {{B, 𝐶}, {A,
B, 𝐶}})) → x ∈ 𝒫
{A, B,
𝐶}) |
18 | 17 | ssriv 2943 |
1
⊢
(({∅, {A}} ∪ {{B}, {A, B}}) ∪ ({{𝐶}, {A,
𝐶}} ∪ {{B, 𝐶}, {A,
B, 𝐶}})) ⊆ 𝒫 {A, B, 𝐶} |