Step |
Hyp |
Ref |
Expression |
1 |
|
diafn.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
diafn.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
diafn.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
4 |
|
diafn.i |
⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
fvex |
⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∈ V |
6 |
5
|
rabex |
⊢ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ∈ V |
7 |
|
eqid |
⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ) = ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ) |
8 |
6 7
|
fnmpti |
⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ) Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } |
9 |
|
eqid |
⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
10 |
|
eqid |
⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) |
11 |
1 2 3 9 10 4
|
diafval |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ) ) |
12 |
11
|
fneq1d |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↔ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ↦ { 𝑓 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∣ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑓 ) ≤ 𝑦 } ) Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ) ) |
13 |
8 12
|
mpbiri |
⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn { 𝑥 ∈ 𝐵 ∣ 𝑥 ≤ 𝑊 } ) |