| Step | Hyp | Ref
| Expression |
| 1 | | dibval3.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
| 2 | | dibval3.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
| 3 | | dibval3.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
| 4 | | dibval3.t |
. . . 4
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 5 | | dibval3.o |
. . . 4
⊢ 0 = (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
| 6 | | eqid 2737 |
. . . 4
⊢
((DIsoA‘𝐾)‘𝑊) = ((DIsoA‘𝐾)‘𝑊) |
| 7 | | dibval3.i |
. . . 4
⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊) |
| 8 | 1, 2, 3, 4, 5, 6, 7 | dibval2 41146 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) = ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × { 0 })) |
| 9 | 8 | eleq2d 2827 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑋) ↔ 𝑌 ∈ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × { 0 }))) |
| 10 | | dibval3.r |
. . . . . . 7
⊢ 𝑅 = ((trL‘𝐾)‘𝑊) |
| 11 | 1, 2, 3, 4, 10, 6 | diaelval 41035 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ↔ (𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ 𝑋))) |
| 12 | 11 | anbi1d 631 |
. . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → ((𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 0 〉) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ 𝑋) ∧ 𝑌 = 〈𝑓, 0 〉))) |
| 13 | | an13 647 |
. . . . . . . 8
⊢ ((𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ (𝑠 ∈ { 0 } ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉))) |
| 14 | | velsn 4642 |
. . . . . . . . 9
⊢ (𝑠 ∈ { 0 } ↔ 𝑠 = 0 ) |
| 15 | 14 | anbi1i 624 |
. . . . . . . 8
⊢ ((𝑠 ∈ { 0 } ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉)) ↔ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉))) |
| 16 | 13, 15 | bitri 275 |
. . . . . . 7
⊢ ((𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ (𝑠 = 0 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉))) |
| 17 | 16 | exbii 1848 |
. . . . . 6
⊢
(∃𝑠(𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ ∃𝑠(𝑠 = 0 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉))) |
| 18 | 4 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝑇 ∈ V |
| 19 | 18 | mptex 7243 |
. . . . . . . 8
⊢ (𝑔 ∈ 𝑇 ↦ ( I ↾ 𝐵)) ∈ V |
| 20 | 5, 19 | eqeltri 2837 |
. . . . . . 7
⊢ 0 ∈
V |
| 21 | | opeq2 4874 |
. . . . . . . . 9
⊢ (𝑠 = 0 → 〈𝑓, 𝑠〉 = 〈𝑓, 0 〉) |
| 22 | 21 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑠 = 0 → (𝑌 = 〈𝑓, 𝑠〉 ↔ 𝑌 = 〈𝑓, 0 〉)) |
| 23 | 22 | anbi2d 630 |
. . . . . . 7
⊢ (𝑠 = 0 → ((𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉) ↔ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 0 〉))) |
| 24 | 20, 23 | ceqsexv 3532 |
. . . . . 6
⊢
(∃𝑠(𝑠 = 0 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 𝑠〉)) ↔ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 0 〉)) |
| 25 | 17, 24 | bitri 275 |
. . . . 5
⊢
(∃𝑠(𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑌 = 〈𝑓, 0 〉)) |
| 26 | | anass 468 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑇 ∧ 𝑌 = 〈𝑓, 0 〉) ∧ (𝑅‘𝑓) ≤ 𝑋) ↔ (𝑓 ∈ 𝑇 ∧ (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋))) |
| 27 | | an32 646 |
. . . . . 6
⊢ (((𝑓 ∈ 𝑇 ∧ 𝑌 = 〈𝑓, 0 〉) ∧ (𝑅‘𝑓) ≤ 𝑋) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ 𝑋) ∧ 𝑌 = 〈𝑓, 0 〉)) |
| 28 | 26, 27 | bitr3i 277 |
. . . . 5
⊢ ((𝑓 ∈ 𝑇 ∧ (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋)) ↔ ((𝑓 ∈ 𝑇 ∧ (𝑅‘𝑓) ≤ 𝑋) ∧ 𝑌 = 〈𝑓, 0 〉)) |
| 29 | 12, 25, 28 | 3bitr4g 314 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (∃𝑠(𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ (𝑓 ∈ 𝑇 ∧ (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋)))) |
| 30 | 29 | exbidv 1921 |
. . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (∃𝑓∃𝑠(𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 })) ↔ ∃𝑓(𝑓 ∈ 𝑇 ∧ (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋)))) |
| 31 | | elxp 5708 |
. . 3
⊢ (𝑌 ∈ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × { 0 }) ↔ ∃𝑓∃𝑠(𝑌 = 〈𝑓, 𝑠〉 ∧ (𝑓 ∈ (((DIsoA‘𝐾)‘𝑊)‘𝑋) ∧ 𝑠 ∈ { 0 }))) |
| 32 | | df-rex 3071 |
. . 3
⊢
(∃𝑓 ∈
𝑇 (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋) ↔ ∃𝑓(𝑓 ∈ 𝑇 ∧ (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋))) |
| 33 | 30, 31, 32 | 3bitr4g 314 |
. 2
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑌 ∈ ((((DIsoA‘𝐾)‘𝑊)‘𝑋) × { 0 }) ↔ ∃𝑓 ∈ 𝑇 (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋))) |
| 34 | 9, 33 | bitrd 279 |
1
⊢ (((𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝑌 ∈ (𝐼‘𝑋) ↔ ∃𝑓 ∈ 𝑇 (𝑌 = 〈𝑓, 0 〉 ∧ (𝑅‘𝑓) ≤ 𝑋))) |