Step | Hyp | Ref
| Expression |
1 | | mptexg 6389 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑉 → (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦)) ∈ V) |
2 | 1 | ralrimivw 2950 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → ∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦)) ∈ V) |
3 | 2 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦)) ∈ V) |
4 | | eqid 2610 |
. . . . . 6
⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦))) = (𝑧 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦))) |
5 | 4 | fnmpt 5933 |
. . . . 5
⊢
(∀𝑧 ∈
{𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} (𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦)) ∈ V → (𝑧 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦))) Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈
2𝑜}) |
6 | 3, 5 | syl 17 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑧 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦))) Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈
2𝑜}) |
7 | | pmtrrn.t |
. . . . . . 7
⊢ 𝑇 = (pmTrsp‘𝐷) |
8 | 7 | pmtrfval 17693 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → 𝑇 = (𝑧 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦)))) |
9 | 8 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → 𝑇 = (𝑧 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦)))) |
10 | 9 | fneq1d 5895 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑇 Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↔ (𝑧 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↦
(𝑦 ∈ 𝐷 ↦ if(𝑦 ∈ 𝑧, ∪ (𝑧 ∖ {𝑦}), 𝑦))) Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈
2𝑜})) |
11 | 6, 10 | mpbird 246 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → 𝑇 Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈
2𝑜}) |
12 | | elpw2g 4754 |
. . . . . 6
⊢ (𝐷 ∈ 𝑉 → (𝑃 ∈ 𝒫 𝐷 ↔ 𝑃 ⊆ 𝐷)) |
13 | 12 | biimpar 501 |
. . . . 5
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷) → 𝑃 ∈ 𝒫 𝐷) |
14 | 13 | 3adant3 1074 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ∈ 𝒫 𝐷) |
15 | | simp3 1056 |
. . . 4
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ≈
2𝑜) |
16 | | breq1 4586 |
. . . . 5
⊢ (𝑥 = 𝑃 → (𝑥 ≈ 2𝑜 ↔ 𝑃 ≈
2𝑜)) |
17 | 16 | elrab 3331 |
. . . 4
⊢ (𝑃 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ↔ (𝑃 ∈ 𝒫 𝐷 ∧ 𝑃 ≈
2𝑜)) |
18 | 14, 15, 17 | sylanbrc 695 |
. . 3
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → 𝑃 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈
2𝑜}) |
19 | | fnfvelrn 6264 |
. . 3
⊢ ((𝑇 Fn {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜} ∧ 𝑃 ∈ {𝑥 ∈ 𝒫 𝐷 ∣ 𝑥 ≈ 2𝑜}) →
(𝑇‘𝑃) ∈ ran 𝑇) |
20 | 11, 18, 19 | syl2anc 691 |
. 2
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑇‘𝑃) ∈ ran 𝑇) |
21 | | pmtrrn.r |
. 2
⊢ 𝑅 = ran 𝑇 |
22 | 20, 21 | syl6eleqr 2699 |
1
⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) →
(𝑇‘𝑃) ∈ 𝑅) |