Step |
Hyp |
Ref |
Expression |
1 |
|
pclfval.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
2 |
|
pclfval.s |
⊢ 𝑆 = ( PSubSp ‘ 𝐾 ) |
3 |
|
pclfval.c |
⊢ 𝑈 = ( PCl ‘ 𝐾 ) |
4 |
|
elex |
⊢ ( 𝐾 ∈ 𝑉 → 𝐾 ∈ V ) |
5 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) ) |
6 |
5 1
|
eqtr4di |
⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 ) |
7 |
6
|
pweqd |
⊢ ( 𝑘 = 𝐾 → 𝒫 ( Atoms ‘ 𝑘 ) = 𝒫 𝐴 ) |
8 |
|
fveq2 |
⊢ ( 𝑘 = 𝐾 → ( PSubSp ‘ 𝑘 ) = ( PSubSp ‘ 𝐾 ) ) |
9 |
8 2
|
eqtr4di |
⊢ ( 𝑘 = 𝐾 → ( PSubSp ‘ 𝑘 ) = 𝑆 ) |
10 |
9
|
rabeqdv |
⊢ ( 𝑘 = 𝐾 → { 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ∣ 𝑥 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) |
11 |
10
|
inteqd |
⊢ ( 𝑘 = 𝐾 → ∩ { 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ∣ 𝑥 ⊆ 𝑦 } = ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) |
12 |
7 11
|
mpteq12dv |
⊢ ( 𝑘 = 𝐾 → ( 𝑥 ∈ 𝒫 ( Atoms ‘ 𝑘 ) ↦ ∩ { 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ∣ 𝑥 ⊆ 𝑦 } ) = ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) ) |
13 |
|
df-pclN |
⊢ PCl = ( 𝑘 ∈ V ↦ ( 𝑥 ∈ 𝒫 ( Atoms ‘ 𝑘 ) ↦ ∩ { 𝑦 ∈ ( PSubSp ‘ 𝑘 ) ∣ 𝑥 ⊆ 𝑦 } ) ) |
14 |
1
|
fvexi |
⊢ 𝐴 ∈ V |
15 |
14
|
pwex |
⊢ 𝒫 𝐴 ∈ V |
16 |
15
|
mptex |
⊢ ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) ∈ V |
17 |
12 13 16
|
fvmpt |
⊢ ( 𝐾 ∈ V → ( PCl ‘ 𝐾 ) = ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) ) |
18 |
3 17
|
syl5eq |
⊢ ( 𝐾 ∈ V → 𝑈 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) ) |
19 |
4 18
|
syl |
⊢ ( 𝐾 ∈ 𝑉 → 𝑈 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) ) |