| Step | Hyp | Ref
| Expression |
| 1 | | df-fm 23946 |
. . . . 5
⊢ FilMap =
(𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦))))) |
| 2 | 1 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))))) |
| 3 | | dmeq 5914 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) |
| 4 | 3 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → (fBas‘dom 𝑓) = (fBas‘dom 𝐹)) |
| 5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (fBas‘dom 𝑓) = (fBas‘dom 𝐹)) |
| 6 | | id 22 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) |
| 7 | | imaeq1 6073 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓 “ 𝑦) = (𝐹 “ 𝑦)) |
| 8 | 7 | mpteq2dv 5244 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)) = (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))) |
| 9 | 8 | rneqd 5949 |
. . . . . . 7
⊢ (𝑓 = 𝐹 → ran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)) = ran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))) |
| 10 | 6, 9 | oveqan12d 7450 |
. . . . . 6
⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦))) = (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) |
| 11 | 5, 10 | mpteq12dv 5233 |
. . . . 5
⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))) = (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))) |
| 12 | | fdm 6745 |
. . . . . . . 8
⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌) |
| 13 | 12 | fveq2d 6910 |
. . . . . . 7
⊢ (𝐹:𝑌⟶𝑋 → (fBas‘dom 𝐹) = (fBas‘𝑌)) |
| 14 | 13 | mpteq1d 5237 |
. . . . . 6
⊢ (𝐹:𝑌⟶𝑋 → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))) |
| 15 | 14 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))) |
| 16 | 11, 15 | sylan9eqr 2799 |
. . . 4
⊢ (((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑥 = 𝑋 ∧ 𝑓 = 𝐹)) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))) |
| 17 | | elex 3501 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ V) |
| 18 | 17 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ V) |
| 19 | | simp3 1139 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐹:𝑌⟶𝑋) |
| 20 | | elfvdm 6943 |
. . . . . 6
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas) |
| 21 | 20 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑌 ∈ dom fBas) |
| 22 | 19, 21 | fexd 7247 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐹 ∈ V) |
| 23 | | fvex 6919 |
. . . . . 6
⊢
(fBas‘𝑌)
∈ V |
| 24 | 23 | mptex 7243 |
. . . . 5
⊢ (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) ∈ V |
| 25 | 24 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) ∈ V) |
| 26 | 2, 16, 18, 22, 25 | ovmpod 7585 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))) |
| 27 | 26 | fveq1d 6908 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵)) |
| 28 | | mpteq1 5235 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)) = (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))) |
| 29 | 28 | rneqd 5949 |
. . . . 5
⊢ (𝑏 = 𝐵 → ran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)) = ran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))) |
| 30 | 29 | oveq2d 7447 |
. . . 4
⊢ (𝑏 = 𝐵 → (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))) |
| 31 | | eqid 2737 |
. . . 4
⊢ (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) |
| 32 | | ovex 7464 |
. . . 4
⊢ (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))) ∈ V |
| 33 | 30, 31, 32 | fvmpt 7016 |
. . 3
⊢ (𝐵 ∈ (fBas‘𝑌) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))) |
| 34 | 33 | 3ad2ant2 1135 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))) |
| 35 | 27, 34 | eqtrd 2777 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))) |