| Step | Hyp | Ref
| Expression |
| 1 | | diaval.i |
. . 3
⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) |
| 2 | | diaval.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
| 3 | | diaval.l |
. . . . 5
⊢ ≤ =
(le‘𝐾) |
| 4 | | diaval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 5 | 2, 3, 4 | diaffval 41032 |
. . . 4
⊢ (𝐾 ∈ 𝑉 → (DIsoA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))) |
| 6 | 5 | fveq1d 6908 |
. . 3
⊢ (𝐾 ∈ 𝑉 → ((DIsoA‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))‘𝑊)) |
| 7 | 1, 6 | eqtrid 2789 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐼 = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))‘𝑊)) |
| 8 | | breq2 5147 |
. . . . 5
⊢ (𝑤 = 𝑊 → (𝑦 ≤ 𝑤 ↔ 𝑦 ≤ 𝑊)) |
| 9 | 8 | rabbidv 3444 |
. . . 4
⊢ (𝑤 = 𝑊 → {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} = {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊}) |
| 10 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
| 11 | | diaval.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 12 | 10, 11 | eqtr4di 2795 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = 𝑇) |
| 13 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → ((trL‘𝐾)‘𝑤) = ((trL‘𝐾)‘𝑊)) |
| 14 | | diaval.r |
. . . . . . . 8
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
| 15 | 13, 14 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ((trL‘𝐾)‘𝑤) = 𝑅) |
| 16 | 15 | fveq1d 6908 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (((trL‘𝐾)‘𝑤)‘𝑓) = (𝑅‘𝑓)) |
| 17 | 16 | breq1d 5153 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥 ↔ (𝑅‘𝑓) ≤ 𝑥)) |
| 18 | 12, 17 | rabeqbidv 3455 |
. . . 4
⊢ (𝑤 = 𝑊 → {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥} = {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥}) |
| 19 | 9, 18 | mpteq12dv 5233 |
. . 3
⊢ (𝑤 = 𝑊 → (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}) = (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊} ↦ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥})) |
| 20 | | eqid 2737 |
. . 3
⊢ (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥})) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥})) |
| 21 | 2 | fvexi 6920 |
. . . 4
⊢ 𝐵 ∈ V |
| 22 | 21 | mptrabex 7245 |
. . 3
⊢ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊} ↦ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥}) ∈ V |
| 23 | 19, 20, 22 | fvmpt 7016 |
. 2
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))‘𝑊) = (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊} ↦ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥})) |
| 24 | 7, 23 | sylan9eq 2797 |
1
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝐼 = (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑊} ↦ {𝑓 ∈ 𝑇 ∣ (𝑅‘𝑓) ≤ 𝑥})) |