Proof of Theorem ex-pw
| Step | Hyp | Ref
| Expression |
| 1 | | pweq 4614 |
. 2
⊢ (𝐴 = {3, 5, 7} → 𝒫
𝐴 = 𝒫 {3, 5,
7}) |
| 2 | | qdass 4753 |
. . . 4
⊢
({∅, {3}} ∪ {{5}, {3, 5}}) = ({∅, {3}, {5}} ∪ {{3,
5}}) |
| 3 | | qdassr 4754 |
. . . 4
⊢ ({{7},
{3, 7}} ∪ {{5, 7}, {3, 5, 7}}) = ({{7}} ∪ {{3, 7}, {5, 7}, {3, 5,
7}}) |
| 4 | 2, 3 | uneq12i 4166 |
. . 3
⊢
(({∅, {3}} ∪ {{5}, {3, 5}}) ∪ ({{7}, {3, 7}} ∪ {{5,
7}, {3, 5, 7}})) = (({∅, {3}, {5}} ∪ {{3, 5}}) ∪ ({{7}} ∪
{{3, 7}, {5, 7}, {3, 5, 7}})) |
| 5 | | pwtp 4902 |
. . 3
⊢ 𝒫
{3, 5, 7} = (({∅, {3}} ∪ {{5}, {3, 5}}) ∪ ({{7}, {3, 7}} ∪
{{5, 7}, {3, 5, 7}})) |
| 6 | | df-tp 4631 |
. . . . . . . 8
⊢ {{3},
{5}, {7}} = ({{3}, {5}} ∪ {{7}}) |
| 7 | 6 | uneq2i 4165 |
. . . . . . 7
⊢
({∅} ∪ {{3}, {5}, {7}}) = ({∅} ∪ ({{3}, {5}} ∪
{{7}})) |
| 8 | | unass 4172 |
. . . . . . 7
⊢
(({∅} ∪ {{3}, {5}}) ∪ {{7}}) = ({∅} ∪ ({{3},
{5}} ∪ {{7}})) |
| 9 | 7, 8 | eqtr4i 2768 |
. . . . . 6
⊢
({∅} ∪ {{3}, {5}, {7}}) = (({∅} ∪ {{3}, {5}}) ∪
{{7}}) |
| 10 | | tpass 4752 |
. . . . . . 7
⊢ {∅,
{3}, {5}} = ({∅} ∪ {{3}, {5}}) |
| 11 | 10 | uneq1i 4164 |
. . . . . 6
⊢
({∅, {3}, {5}} ∪ {{7}}) = (({∅} ∪ {{3}, {5}}) ∪
{{7}}) |
| 12 | 9, 11 | eqtr4i 2768 |
. . . . 5
⊢
({∅} ∪ {{3}, {5}, {7}}) = ({∅, {3}, {5}} ∪
{{7}}) |
| 13 | | unass 4172 |
. . . . . 6
⊢ (({{3,
5}} ∪ {{3, 7}, {5, 7}}) ∪ {{3, 5, 7}}) = ({{3, 5}} ∪ ({{3, 7}, {5,
7}} ∪ {{3, 5, 7}})) |
| 14 | | tpass 4752 |
. . . . . . 7
⊢ {{3, 5},
{3, 7}, {5, 7}} = ({{3, 5}} ∪ {{3, 7}, {5, 7}}) |
| 15 | 14 | uneq1i 4164 |
. . . . . 6
⊢ ({{3, 5},
{3, 7}, {5, 7}} ∪ {{3, 5, 7}}) = (({{3, 5}} ∪ {{3, 7}, {5, 7}}) ∪
{{3, 5, 7}}) |
| 16 | | df-tp 4631 |
. . . . . . 7
⊢ {{3, 7},
{5, 7}, {3, 5, 7}} = ({{3, 7}, {5, 7}} ∪ {{3, 5, 7}}) |
| 17 | 16 | uneq2i 4165 |
. . . . . 6
⊢ ({{3, 5}}
∪ {{3, 7}, {5, 7}, {3, 5, 7}}) = ({{3, 5}} ∪ ({{3, 7}, {5, 7}} ∪
{{3, 5, 7}})) |
| 18 | 13, 15, 17 | 3eqtr4i 2775 |
. . . . 5
⊢ ({{3, 5},
{3, 7}, {5, 7}} ∪ {{3, 5, 7}}) = ({{3, 5}} ∪ {{3, 7}, {5, 7}, {3, 5,
7}}) |
| 19 | 12, 18 | uneq12i 4166 |
. . . 4
⊢
(({∅} ∪ {{3}, {5}, {7}}) ∪ ({{3, 5}, {3, 7}, {5, 7}} ∪
{{3, 5, 7}})) = (({∅, {3}, {5}} ∪ {{7}}) ∪ ({{3, 5}} ∪ {{3,
7}, {5, 7}, {3, 5, 7}})) |
| 20 | | un4 4175 |
. . . 4
⊢
(({∅, {3}, {5}} ∪ {{3, 5}}) ∪ ({{7}} ∪ {{3, 7}, {5,
7}, {3, 5, 7}})) = (({∅, {3}, {5}} ∪ {{7}}) ∪ ({{3, 5}} ∪
{{3, 7}, {5, 7}, {3, 5, 7}})) |
| 21 | 19, 20 | eqtr4i 2768 |
. . 3
⊢
(({∅} ∪ {{3}, {5}, {7}}) ∪ ({{3, 5}, {3, 7}, {5, 7}} ∪
{{3, 5, 7}})) = (({∅, {3}, {5}} ∪ {{3, 5}}) ∪ ({{7}} ∪ {{3,
7}, {5, 7}, {3, 5, 7}})) |
| 22 | 4, 5, 21 | 3eqtr4i 2775 |
. 2
⊢ 𝒫
{3, 5, 7} = (({∅} ∪ {{3}, {5}, {7}}) ∪ ({{3, 5}, {3, 7}, {5, 7}}
∪ {{3, 5, 7}})) |
| 23 | 1, 22 | eqtrdi 2793 |
1
⊢ (𝐴 = {3, 5, 7} → 𝒫
𝐴 = (({∅} ∪ {{3},
{5}, {7}}) ∪ ({{3, 5}, {3, 7}, {5, 7}} ∪ {{3, 5,
7}}))) |