Metamath Proof Explorer


Theorem pclfvalN

Description: The projective subspace closure function. (Contributed by NM, 7-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclfval.a 𝐴 = ( Atoms ‘ 𝐾 )
pclfval.s 𝑆 = ( PSubSp ‘ 𝐾 )
pclfval.c 𝑈 = ( PCl ‘ 𝐾 )
Assertion pclfvalN ( 𝐾𝑉𝑈 = ( 𝑥 ∈ 𝒫 𝐴 { 𝑦𝑆𝑥𝑦 } ) )

Proof

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 ( 𝐾𝑉𝑈 = ( 𝑥 ∈ 𝒫 𝐴 { 𝑦𝑆𝑥𝑦 } ) )