| Step | Hyp | Ref
| Expression |
| 1 | | docaval.n |
. . 3
⊢ 𝑁 = ((ocA‘𝐾)‘𝑊) |
| 2 | | docaval.j |
. . . . 5
⊢ ∨ =
(join‘𝐾) |
| 3 | | docaval.m |
. . . . 5
⊢ ∧ =
(meet‘𝐾) |
| 4 | | docaval.o |
. . . . 5
⊢ ⊥ =
(oc‘𝐾) |
| 5 | | docaval.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 6 | 2, 3, 4, 5 | docaffvalN 41123 |
. . . 4
⊢ (𝐾 ∈ 𝑉 → (ocA‘𝐾) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))))) |
| 7 | 6 | fveq1d 6908 |
. . 3
⊢ (𝐾 ∈ 𝑉 → ((ocA‘𝐾)‘𝑊) = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))))‘𝑊)) |
| 8 | 1, 7 | eqtrid 2789 |
. 2
⊢ (𝐾 ∈ 𝑉 → 𝑁 = ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))))‘𝑊)) |
| 9 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = ((LTrn‘𝐾)‘𝑊)) |
| 10 | | docaval.t |
. . . . . 6
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 11 | 9, 10 | eqtr4di 2795 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((LTrn‘𝐾)‘𝑤) = 𝑇) |
| 12 | 11 | pweqd 4617 |
. . . 4
⊢ (𝑤 = 𝑊 → 𝒫 ((LTrn‘𝐾)‘𝑤) = 𝒫 𝑇) |
| 13 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 𝑊 → ((DIsoA‘𝐾)‘𝑤) = ((DIsoA‘𝐾)‘𝑊)) |
| 14 | | docaval.i |
. . . . . 6
⊢ 𝐼 = ((DIsoA‘𝐾)‘𝑊) |
| 15 | 13, 14 | eqtr4di 2795 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((DIsoA‘𝐾)‘𝑤) = 𝐼) |
| 16 | 15 | cnveqd 5886 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ◡((DIsoA‘𝐾)‘𝑤) = ◡𝐼) |
| 17 | 15 | rneqd 5949 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑊 → ran ((DIsoA‘𝐾)‘𝑤) = ran 𝐼) |
| 18 | 17 | rabeqdv 3452 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧} = {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧}) |
| 19 | 18 | inteqd 4951 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → ∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧} = ∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧}) |
| 20 | 16, 19 | fveq12d 6913 |
. . . . . . . 8
⊢ (𝑤 = 𝑊 → (◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧}) = (◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧})) |
| 21 | 20 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) = ( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧}))) |
| 22 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → ( ⊥ ‘𝑤) = ( ⊥ ‘𝑊)) |
| 23 | 21, 22 | oveq12d 7449 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) = (( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊))) |
| 24 | | id 22 |
. . . . . 6
⊢ (𝑤 = 𝑊 → 𝑤 = 𝑊) |
| 25 | 23, 24 | oveq12d 7449 |
. . . . 5
⊢ (𝑤 = 𝑊 → ((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤) = ((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)) |
| 26 | 15, 25 | fveq12d 6913 |
. . . 4
⊢ (𝑤 = 𝑊 → (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤)) = (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊))) |
| 27 | 12, 26 | mpteq12dv 5233 |
. . 3
⊢ (𝑤 = 𝑊 → (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))) = (𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))) |
| 28 | | eqid 2737 |
. . 3
⊢ (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤)))) = (𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤)))) |
| 29 | 10 | fvexi 6920 |
. . . . 5
⊢ 𝑇 ∈ V |
| 30 | 29 | pwex 5380 |
. . . 4
⊢ 𝒫
𝑇 ∈ V |
| 31 | 30 | mptex 7243 |
. . 3
⊢ (𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊))) ∈ V |
| 32 | 27, 28, 31 | fvmpt 7016 |
. 2
⊢ (𝑊 ∈ 𝐻 → ((𝑤 ∈ 𝐻 ↦ (𝑥 ∈ 𝒫 ((LTrn‘𝐾)‘𝑤) ↦ (((DIsoA‘𝐾)‘𝑤)‘((( ⊥ ‘(◡((DIsoA‘𝐾)‘𝑤)‘∩ {𝑧 ∈ ran ((DIsoA‘𝐾)‘𝑤) ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑤)) ∧ 𝑤))))‘𝑊) = (𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))) |
| 33 | 8, 32 | sylan9eq 2797 |
1
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) → 𝑁 = (𝑥 ∈ 𝒫 𝑇 ↦ (𝐼‘((( ⊥ ‘(◡𝐼‘∩ {𝑧 ∈ ran 𝐼 ∣ 𝑥 ⊆ 𝑧})) ∨ ( ⊥ ‘𝑊)) ∧ 𝑊)))) |