| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝐾 ∈ 𝐵 → 𝐾 ∈ V) |
| 2 | | dilset.l |
. . 3
⊢ 𝐿 = (Dil‘𝐾) |
| 3 | | fveq2 6906 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) |
| 4 | | dilset.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
| 5 | 3, 4 | eqtr4di 2795 |
. . . . 5
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) |
| 6 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (PAut‘𝑘) = (PAut‘𝐾)) |
| 7 | | dilset.m |
. . . . . . 7
⊢ 𝑀 = (PAut‘𝐾) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (PAut‘𝑘) = 𝑀) |
| 9 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (PSubSp‘𝑘) = (PSubSp‘𝐾)) |
| 10 | | dilset.s |
. . . . . . . 8
⊢ 𝑆 = (PSubSp‘𝐾) |
| 11 | 9, 10 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (PSubSp‘𝑘) = 𝑆) |
| 12 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (WAtoms‘𝑘) = (WAtoms‘𝐾)) |
| 13 | | dilset.w |
. . . . . . . . . . 11
⊢ 𝑊 = (WAtoms‘𝐾) |
| 14 | 12, 13 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (WAtoms‘𝑘) = 𝑊) |
| 15 | 14 | fveq1d 6908 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → ((WAtoms‘𝑘)‘𝑑) = (𝑊‘𝑑)) |
| 16 | 15 | sseq2d 4016 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) ↔ 𝑥 ⊆ (𝑊‘𝑑))) |
| 17 | 16 | imbi1d 341 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥) ↔ (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥))) |
| 18 | 11, 17 | raleqbidv 3346 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥) ↔ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥))) |
| 19 | 8, 18 | rabeqbidv 3455 |
. . . . 5
⊢ (𝑘 = 𝐾 → {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)} = {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)}) |
| 20 | 5, 19 | mpteq12dv 5233 |
. . . 4
⊢ (𝑘 = 𝐾 → (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)}) = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)})) |
| 21 | | df-dilN 40108 |
. . . 4
⊢ Dil =
(𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)})) |
| 22 | 20, 21, 4 | mptfvmpt 7248 |
. . 3
⊢ (𝐾 ∈ V →
(Dil‘𝐾) = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)})) |
| 23 | 2, 22 | eqtrid 2789 |
. 2
⊢ (𝐾 ∈ V → 𝐿 = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)})) |
| 24 | 1, 23 | syl 17 |
1
⊢ (𝐾 ∈ 𝐵 → 𝐿 = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)})) |