This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqtrid ⊢ ( 𝐾 ∈ V → 𝑈 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) )
19 4 18 syl ⊢ ( 𝐾 ∈ 𝑉 → 𝑈 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) )