Step | Hyp | Ref
| Expression |
1 | | pmtrfval.t |
. . . . 5
⊢ 𝑇 = (pmTrsp‘𝐷) |
2 | 1 | pmtrfval 17693 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → 𝑇 = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) |
3 | 2 | fveq1d 6105 |
. . 3
⊢ (𝐷 ∈ 𝑉 → (𝑇‘𝑃) = ((𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))‘𝑃)) |
4 | 3 | 3ad2ant1 1075 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑇‘𝑃) = ((𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))‘𝑃)) |
5 | | elpw2g 4754 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → (𝑃 ∈ 𝒫 𝐷 ↔ 𝑃 ⊆ 𝐷)) |
6 | 5 | biimpar 501 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷) → 𝑃 ∈ 𝒫 𝐷) |
7 | 6 | 3adant3 1074 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ∈ 𝒫 𝐷) |
8 | | simp3 1056 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ≈
2𝑜) |
9 | | breq1 4586 |
. . . . 5
⊢ (𝑦 = 𝑃 → (𝑦 ≈ 2𝑜 ↔ 𝑃 ≈
2𝑜)) |
10 | 9 | elrab 3331 |
. . . 4
⊢ (𝑃 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2𝑜} ↔ (𝑃 ∈ 𝒫 𝐷 ∧ 𝑃 ≈
2𝑜)) |
11 | 7, 8, 10 | sylanbrc 695 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈
2𝑜}) |
12 | | mptexg 6389 |
. . . 4
⊢ (𝐷 ∈ 𝑉 → (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧)) ∈ V) |
13 | 12 | 3ad2ant1 1075 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧)) ∈ V) |
14 | | eleq2 2677 |
. . . . . 6
⊢ (𝑝 = 𝑃 → (𝑧 ∈ 𝑝 ↔ 𝑧 ∈ 𝑃)) |
15 | | difeq1 3683 |
. . . . . . 7
⊢ (𝑝 = 𝑃 → (𝑝 ∖ {𝑧}) = (𝑃 ∖ {𝑧})) |
16 | 15 | unieqd 4382 |
. . . . . 6
⊢ (𝑝 = 𝑃 → ∪ (𝑝 ∖ {𝑧}) = ∪ (𝑃 ∖ {𝑧})) |
17 | 14, 16 | ifbieq1d 4059 |
. . . . 5
⊢ (𝑝 = 𝑃 → if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧) = if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧)) |
18 | 17 | mpteq2dv 4673 |
. . . 4
⊢ (𝑝 = 𝑃 → (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧))) |
19 | | eqid 2610 |
. . . 4
⊢ (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))) |
20 | 18, 19 | fvmptg 6189 |
. . 3
⊢ ((𝑃 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2𝑜} ∧ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧)) ∈ V) → ((𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧))) |
21 | 11, 13, 20 | syl2anc 691 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
((𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2𝑜} ↦
(𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧))) |
22 | 4, 21 | eqtrd 2644 |
1
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑇‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧))) |