Step |
Hyp |
Ref |
Expression |
1 |
|
ldilset.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
ldilset.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
ldilset.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
4 |
|
ldilset.i |
⊢ 𝐼 = ( LAut ‘ 𝐾 ) |
5 |
|
elex |
⊢ ( 𝐾 ∈ 𝐶 → 𝐾 ∈ V ) |
6 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) ) |
7 |
6 3
|
eqtr4di |
⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 ) |
8 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( LAut ‘ 𝑘 ) = ( LAut ‘ 𝐾 ) ) |
9 |
8 4
|
eqtr4di |
⊢ ( 𝑘 = 𝐾 → ( LAut ‘ 𝑘 ) = 𝐼 ) |
10 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = ( Base ‘ 𝐾 ) ) |
11 |
10 1
|
eqtr4di |
⊢ ( 𝑘 = 𝐾 → ( Base ‘ 𝑘 ) = 𝐵 ) |
12 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) ) |
13 |
12 2
|
eqtr4di |
⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ ) |
14 |
13
|
breqd |
⊢ ( 𝑘 = 𝐾 → ( 𝑥 ( le ‘ 𝑘 ) 𝑤 ↔ 𝑥 ≤ 𝑤 ) ) |
15 |
14
|
imbi1d |
⊢ ( 𝑘 = 𝐾 → ( ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ↔ ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ) ) |
16 |
11 15
|
raleqbidv |
⊢ ( 𝑘 = 𝐾 → ( ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) ) ) |
17 |
9 16
|
rabeqbidv |
⊢ ( 𝑘 = 𝐾 → { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } = { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) |
18 |
7 17
|
mpteq12dv |
⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) ) |
19 |
|
df-ldil |
⊢ LDil = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ { 𝑓 ∈ ( LAut ‘ 𝑘 ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑘 ) ( 𝑥 ( le ‘ 𝑘 ) 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) ) |
20 |
18 19 3
|
mptfvmpt |
⊢ ( 𝐾 ∈ V → ( LDil ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) ) |
21 |
5 20
|
syl |
⊢ ( 𝐾 ∈ 𝐶 → ( LDil ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ { 𝑓 ∈ 𝐼 ∣ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ≤ 𝑤 → ( 𝑓 ‘ 𝑥 ) = 𝑥 ) } ) ) |