| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
| 2 | | fveq2 6906 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
| 3 | | diaval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
| 5 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = (Base‘𝐾)) |
| 6 | | diaval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
| 7 | 5, 6 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (Base‘𝑘) = 𝐵) |
| 8 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) |
| 9 | | diaval.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝐾) |
| 10 | 8, 9 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) |
| 11 | 10 | breqd 5154 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑦(le‘𝑘)𝑤 ↔ 𝑦 ≤ 𝑤)) |
| 12 | 7, 11 | rabeqbidv 3455 |
. . . . 5
⊢ (𝑘 = 𝐾 → {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} = {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤}) |
| 13 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
| 14 | 13 | fveq1d 6908 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
| 15 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (trL‘𝑘) = (trL‘𝐾)) |
| 16 | 15 | fveq1d 6908 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((trL‘𝑘)‘𝑤) = ((trL‘𝐾)‘𝑤)) |
| 17 | 16 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (((trL‘𝑘)‘𝑤)‘𝑓) = (((trL‘𝐾)‘𝑤)‘𝑓)) |
| 18 | | eqidd 2738 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → 𝑥 = 𝑥) |
| 19 | 17, 10, 18 | breq123d 5157 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥 ↔ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥)) |
| 20 | 14, 19 | rabeqbidv 3455 |
. . . . 5
⊢ (𝑘 = 𝐾 → {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥} = {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}) |
| 21 | 12, 20 | mpteq12dv 5233 |
. . . 4
⊢ (𝑘 = 𝐾 → (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}) = (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥})) |
| 22 | 4, 21 | mpteq12dv 5233 |
. . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥})) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))) |
| 23 | | df-disoa 41031 |
. . 3
⊢ DIsoA =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ {𝑦 ∈ (Base‘𝑘) ∣ 𝑦(le‘𝑘)𝑤} ↦ {𝑓 ∈ ((LTrn‘𝑘)‘𝑤) ∣ (((trL‘𝑘)‘𝑤)‘𝑓)(le‘𝑘)𝑥}))) |
| 24 | 22, 23, 3 | mptfvmpt 7248 |
. 2
⊢ (𝐾 ∈ V →
(DIsoA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))) |
| 25 | 1, 24 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → (DIsoA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ {𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑤} ↦ {𝑓 ∈ ((LTrn‘𝐾)‘𝑤) ∣ (((trL‘𝐾)‘𝑤)‘𝑓) ≤ 𝑥}))) |