| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
| 2 | | fveq2 6906 |
. . . . 5
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = (LHyp‘𝐾)) |
| 3 | | docaval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . 4
⊢ (𝑘 = 𝐾 → (LHyp‘𝑘) = 𝐻) |
| 5 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (LTrn‘𝑘) = (LTrn‘𝐾)) |
| 6 | 5 | fveq1d 6908 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((LTrn‘𝑘)‘𝑤) = ((LTrn‘𝐾)‘𝑤)) |
| 7 | 6 | pweqd 4617 |
. . . . 5
⊢ (𝑘 = 𝐾 → 𝒫 ((LTrn‘𝑘)‘𝑤) = 𝒫 ((LTrn‘𝐾)‘𝑤)) |
| 8 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (DIsoA‘𝑘) = (DIsoA‘𝐾)) |
| 9 | 8 | fveq1d 6908 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((DIsoA‘𝑘)‘𝑤) = ((DIsoA‘𝐾)‘𝑤)) |
| 10 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = (meet‘𝐾)) |
| 11 | | docaval.m |
. . . . . . . 8
⊢ ∧ =
(meet‘𝐾) |
| 12 | 10, 11 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (meet‘𝑘) = ∧ ) |
| 13 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (join‘𝑘) = (join‘𝐾)) |
| 14 | | docaval.j |
. . . . . . . . 9
⊢ ∨ =
(join‘𝐾) |
| 15 | 13, 14 | eqtr4di 2795 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → (join‘𝑘) = ∨ ) |
| 16 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → (oc‘𝑘) = (oc‘𝐾)) |
| 17 | | docaval.o |
. . . . . . . . . 10
⊢ ⊥ =
(oc‘𝐾) |
| 18 | 16, 17 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (oc‘𝑘) = ⊥ ) |
| 19 | 9 | cnveqd 5886 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → ◡((DIsoA‘𝑘)‘𝑤) = ◡((DIsoA‘𝐾)‘𝑤)) |
| 20 | 9 | rneqd 5949 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝐾 → ran ((DIsoA‘𝑘)‘𝑤) = ran ((DIsoA‘𝐾)‘𝑤)) |
| 21 | 20 | rabeqdv 3452 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝐾 → {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧} = {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧}) |
| 22 | 21 | inteqd 4951 |
. . . . . . . . . 10
⊢ (𝑘 = 𝐾 → ∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧} = ∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧}) |
| 23 | 19, 22 | fveq12d 6913 |
. . . . . . . . 9
⊢ (𝑘 = 𝐾 → (◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}) = (◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) |
| 24 | 18, 23 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) = ( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))) |
| 25 | 18 | fveq1d 6908 |
. . . . . . . 8
⊢ (𝑘 = 𝐾 → ((oc‘𝑘)‘𝑤) = ( ⊥ ‘𝑤)) |
| 26 | 15, 24, 25 | oveq123d 7452 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → (((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤)) = (( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤))) |
| 27 | | eqidd 2738 |
. . . . . . 7
⊢ (𝑘 = 𝐾 → 𝑤 = 𝑤) |
| 28 | 12, 26, 27 | oveq123d 7452 |
. . . . . 6
⊢ (𝑘 = 𝐾 → ((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤) = ((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤)) |
| 29 | 9, 28 | fveq12d 6913 |
. . . . 5
⊢ (𝑘 = 𝐾 → (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)) = (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))) |
| 30 | 7, 29 | mpteq12dv 5233 |
. . . 4
⊢ (𝑘 = 𝐾 → (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))) = (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤)))) |
| 31 | 4, 30 | mpteq12dv 5233 |
. . 3
⊢ (𝑘 = 𝐾 → (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤)))) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))))) |
| 32 | | df-docaN 41122 |
. . 3
⊢ ocA =
(𝑘 ∈ V ↦ (𝑤 ∈ (LHyp‘𝑘) ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝑘)‘𝑤) ↦ (((DIsoA‘𝑘)‘𝑤)‘((((oc‘𝑘)‘(◡((DIsoA‘𝑘)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝑘)‘𝑤) ∣ 𝑥 ⊆ 𝑧}))(join‘𝑘)((oc‘𝑘)‘𝑤))(meet‘𝑘)𝑤))))) |
| 33 | 31, 32, 3 | mptfvmpt 7248 |
. 2
⊢ (𝐾 ∈ V →
(ocA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))))) |
| 34 | 1, 33 | syl 17 |
1
⊢ (𝐾 ∈ 𝑉 → (ocA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))))) |