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