Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. 2
⊢ (𝐾 ∈ 𝐵 → 𝐾 ∈ V) |
2 | | dilset.l |
. . 3
⊢ 𝐿 = (Dil‘𝐾) |
3 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) |
4 | | dilset.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
5 | 3, 4 | syl6eqr 2662 |
. . . . 5
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) |
6 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (PAut‘𝑘) = (PAut‘𝐾)) |
7 | | dilset.m |
. . . . . . 7
⊢ 𝑀 = (PAut‘𝐾) |
8 | 6, 7 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (PAut‘𝑘) = 𝑀) |
9 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (PSubSp‘𝑘) = (PSubSp‘𝐾)) |
10 | | dilset.s |
. . . . . . . 8
⊢ 𝑆 = (PSubSp‘𝐾) |
11 | 9, 10 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (PSubSp‘𝑘) = 𝑆) |
12 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (WAtoms‘𝑘) = (WAtoms‘𝐾)) |
13 | | dilset.w |
. . . . . . . . . . 11
⊢ 𝑊 = (WAtoms‘𝐾) |
14 | 12, 13 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (WAtoms‘𝑘) = 𝑊) |
15 | 14 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → ((WAtoms‘𝑘)‘𝑑) = (𝑊‘𝑑)) |
16 | 15 | sseq2d 3596 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) ↔ 𝑥 ⊆ (𝑊‘𝑑))) |
17 | 16 | imbi1d 330 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → ((𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥) ↔ (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥))) |
18 | 11, 17 | raleqbidv 3129 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥) ↔ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥))) |
19 | 8, 18 | rabeqbidv 3168 |
. . . . 5
⊢ (𝑘 = 𝐾 → {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)} = {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)}) |
20 | 5, 19 | mpteq12dv 4663 |
. . . 4
⊢ (𝑘 = 𝐾 → (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)}) = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)})) |
21 | | df-dilN 34410 |
. . . 4
⊢ Dil =
(𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ {𝑓 ∈ (PAut‘𝑘) ∣ ∀𝑥 ∈ (PSubSp‘𝑘)(𝑥 ⊆ ((WAtoms‘𝑘)‘𝑑) → (𝑓‘𝑥) = 𝑥)})) |
22 | | fvex 6113 |
. . . . . 6
⊢
(Atoms‘𝐾)
∈ V |
23 | 4, 22 | eqeltri 2684 |
. . . . 5
⊢ 𝐴 ∈ V |
24 | 23 | mptex 6390 |
. . . 4
⊢ (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)}) ∈ V |
25 | 20, 21, 24 | fvmpt 6191 |
. . 3
⊢ (𝐾 ∈ V →
(Dil‘𝐾) = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)})) |
26 | 2, 25 | syl5eq 2656 |
. 2
⊢ (𝐾 ∈ V → 𝐿 = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)})) |
27 | 1, 26 | syl 17 |
1
⊢ (𝐾 ∈ 𝐵 → 𝐿 = (𝑑 ∈ 𝐴 ↦ {𝑓 ∈ 𝑀 ∣ ∀𝑥 ∈ 𝑆 (𝑥 ⊆ (𝑊‘𝑑) → (𝑓‘𝑥) = 𝑥)})) |