Step | Hyp | Ref
| Expression |
1 | | snex 4908 |
. . 3
⊢ {𝐴} ∈ V |
2 | | eqid 2622 |
. . . 4
⊢
(pmTrsp‘{𝐴}) =
(pmTrsp‘{𝐴}) |
3 | 2 | pmtrfval 17870 |
. . 3
⊢ ({𝐴} ∈ V →
(pmTrsp‘{𝐴}) = (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
4 | 1, 3 | ax-mp 5 |
. 2
⊢
(pmTrsp‘{𝐴}) =
(𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
5 | | eqid 2622 |
. . . . 5
⊢ (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
6 | 5 | dmmpt 5630 |
. . . 4
⊢ dom
(𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = {𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ∣
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) ∈ V} |
7 | | 2on0 7569 |
. . . . . . . . 9
⊢
2𝑜 ≠ ∅ |
8 | | ensymb 8004 |
. . . . . . . . . 10
⊢ (∅
≈ 2𝑜 ↔ 2𝑜 ≈
∅) |
9 | | en0 8019 |
. . . . . . . . . 10
⊢
(2𝑜 ≈ ∅ ↔ 2𝑜 =
∅) |
10 | 8, 9 | bitri 264 |
. . . . . . . . 9
⊢ (∅
≈ 2𝑜 ↔ 2𝑜 =
∅) |
11 | 7, 10 | nemtbir 2889 |
. . . . . . . 8
⊢ ¬
∅ ≈ 2𝑜 |
12 | | snnen2o 8149 |
. . . . . . . 8
⊢ ¬
{𝐴} ≈
2𝑜 |
13 | | 0ex 4790 |
. . . . . . . . 9
⊢ ∅
∈ V |
14 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → (𝑦 ≈ 2𝑜
↔ ∅ ≈ 2𝑜)) |
15 | 14 | notbid 308 |
. . . . . . . . 9
⊢ (𝑦 = ∅ → (¬ 𝑦 ≈ 2𝑜
↔ ¬ ∅ ≈ 2𝑜)) |
16 | | breq1 4656 |
. . . . . . . . . 10
⊢ (𝑦 = {𝐴} → (𝑦 ≈ 2𝑜 ↔ {𝐴} ≈
2𝑜)) |
17 | 16 | notbid 308 |
. . . . . . . . 9
⊢ (𝑦 = {𝐴} → (¬ 𝑦 ≈ 2𝑜 ↔ ¬
{𝐴} ≈
2𝑜)) |
18 | 13, 1, 15, 17 | ralpr 4238 |
. . . . . . . 8
⊢
(∀𝑦 ∈
{∅, {𝐴}} ¬ 𝑦 ≈ 2𝑜
↔ (¬ ∅ ≈ 2𝑜 ∧ ¬ {𝐴} ≈
2𝑜)) |
19 | 11, 12, 18 | mpbir2an 955 |
. . . . . . 7
⊢
∀𝑦 ∈
{∅, {𝐴}} ¬ 𝑦 ≈
2𝑜 |
20 | | pwsn 4428 |
. . . . . . . 8
⊢ 𝒫
{𝐴} = {∅, {𝐴}} |
21 | 20 | raleqi 3142 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝒫 {𝐴} ¬ 𝑦 ≈ 2𝑜
↔ ∀𝑦 ∈
{∅, {𝐴}} ¬ 𝑦 ≈
2𝑜) |
22 | 19, 21 | mpbir 221 |
. . . . . 6
⊢
∀𝑦 ∈
𝒫 {𝐴} ¬ 𝑦 ≈
2𝑜 |
23 | | rabeq0 3957 |
. . . . . 6
⊢ ({𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} = ∅
↔ ∀𝑦 ∈
𝒫 {𝐴} ¬ 𝑦 ≈
2𝑜) |
24 | 22, 23 | mpbir 221 |
. . . . 5
⊢ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} =
∅ |
25 | | rabeq 3192 |
. . . . 5
⊢ ({𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} = ∅
→ {𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ∣
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) ∈ V} = {𝑝 ∈ ∅ ∣ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) ∈ V}) |
26 | 24, 25 | ax-mp 5 |
. . . 4
⊢ {𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ∣
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) ∈ V} = {𝑝 ∈ ∅ ∣ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) ∈ V} |
27 | | rab0 3955 |
. . . 4
⊢ {𝑝 ∈ ∅ ∣ (𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) ∈ V} = ∅ |
28 | 6, 26, 27 | 3eqtri 2648 |
. . 3
⊢ dom
(𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅ |
29 | | funmpt 5926 |
. . . . 5
⊢ Fun
(𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
30 | | funrel 5905 |
. . . . 5
⊢ (Fun
(𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → Rel (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
31 | 29, 30 | ax-mp 5 |
. . . 4
⊢ Rel
(𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
32 | | reldm0 5343 |
. . . 4
⊢ (Rel
(𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) → ((𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅ ↔ dom (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅)) |
33 | 31, 32 | ax-mp 5 |
. . 3
⊢ ((𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅ ↔ dom (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅) |
34 | 28, 33 | mpbir 221 |
. 2
⊢ (𝑝 ∈ {𝑦 ∈ 𝒫 {𝐴} ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ {𝐴} ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = ∅ |
35 | 4, 34 | eqtri 2644 |
1
⊢
(pmTrsp‘{𝐴}) =
∅ |