Step | Hyp | Ref
| Expression |
1 | | elex 3449 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
2 | | fveq2 6771 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
3 | | dicval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
4 | 2, 3 | eqtr4di 2798 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
5 | | fveq2 6771 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = (Atoms‘𝐾)) |
6 | | dicval.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
7 | 5, 6 | eqtr4di 2798 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (Atoms‘𝑘) = 𝐴) |
8 | | fveq2 6771 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (le‘𝑘) = (le‘𝐾)) |
9 | | dicval.l |
. . . . . . . . 9
⊢ ≤ =
(le‘𝐾) |
10 | 8, 9 | eqtr4di 2798 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (le‘𝑘) = ≤ ) |
11 | 10 | breqd 5090 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑟(le‘𝑘)𝑤 ↔ 𝑟 ≤ 𝑤)) |
12 | 11 | notbid 318 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (¬ 𝑟(le‘𝑘)𝑤 ↔ ¬ 𝑟 ≤ 𝑤)) |
13 | 7, 12 | rabeqbidv 3419 |
. . . . 5
⊢ (𝑘 = 𝐾 → {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} = {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤}) |
14 | | fveq2 6771 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
15 | 14 | fveq1d 6773 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
16 | | fveq2 6771 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → (oc‘𝑘) = (oc‘𝐾)) |
17 | 16 | fveq1d 6773 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → ((oc‘𝑘)‘𝑤) = ((oc‘𝐾)‘𝑤)) |
18 | 17 | fveqeq2d 6779 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → ((𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞 ↔ (𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) |
19 | 15, 18 | riotaeqbidv 7231 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞) = (℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) |
20 | 19 | fveq2d 6775 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞))) |
21 | 20 | eqeq2d 2751 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ↔ 𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)))) |
22 | | fveq2 6771 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (TEndo‘𝑘) = (TEndo‘𝐾)) |
23 | 22 | fveq1d 6773 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((TEndo‘𝑘)‘𝑤) = ((TEndo‘𝐾)‘𝑤)) |
24 | 23 | eleq2d 2826 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (𝑠 ∈ ((TEndo‘𝑘)‘𝑤) ↔ 𝑠 ∈ ((TEndo‘𝐾)‘𝑤))) |
25 | 21, 24 | anbi12d 631 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤)) ↔ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑤)))) |
26 | 25 | opabbidv 5145 |
. . . . 5
⊢ (𝑘 = 𝐾 → {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))} = {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑤))}) |
27 | 13, 26 | mpteq12dv 5170 |
. . . 4
⊢ (𝑘 = 𝐾 → (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))}) = (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑤))})) |
28 | 4, 27 | mpteq12dv 5170 |
. . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))})) = (𝑤 ∈ 𝐻 ↦ (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑤))}))) |
29 | | df-dic 39183 |
. . 3
⊢ DIsoC =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑞 ∈ {𝑟 ∈ (Atoms‘𝑘) ∣ ¬ 𝑟(le‘𝑘)𝑤} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝑘)‘𝑤)(𝑔‘((oc‘𝑘)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝑘)‘𝑤))}))) |
30 | 28, 29, 3 | mptfvmpt 7101 |
. 2
⊢ (𝐾 ∈ V →
(DIsoC‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑤))}))) |
31 | 1, 30 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → (DIsoC‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑞 ∈ {𝑟 ∈ 𝐴 ∣ ¬ 𝑟 ≤ 𝑤} ↦ {〈𝑓, 𝑠〉 ∣ (𝑓 = (𝑠‘(℩𝑔 ∈ ((LTrn‘𝐾)‘𝑤)(𝑔‘((oc‘𝐾)‘𝑤)) = 𝑞)) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑤))}))) |