Theorem pclvalN

Description: Value of 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	pclvalN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) = ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		pclfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		pclfval.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3		pclfval.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
4	1	fvexi	⊢ 𝐴 ∈ V
5	4	elpw2	⊢ ( 𝑋 ∈ 𝒫 𝐴 ↔ 𝑋 ⊆ 𝐴 )
6	1 2 3	pclfvalN	⊢ ( 𝐾 ∈ 𝑉 → 𝑈 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) )
7	6	fveq1d	⊢ ( 𝐾 ∈ 𝑉 → ( 𝑈 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) ‘ 𝑋 ) )
8	7	adantr	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴 ) → ( 𝑈 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) ‘ 𝑋 ) )
9		eqid	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) = ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } )
10		sseq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝑦 ) )
11	10	rabbidv	⊢ ( 𝑥 = 𝑋 → { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } = { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )
12	11	inteqd	⊢ ( 𝑥 = 𝑋 → ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } = ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )
13		simpr	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴 ) → 𝑋 ∈ 𝒫 𝐴 )
14		elpwi	⊢ ( 𝑋 ∈ 𝒫 𝐴 → 𝑋 ⊆ 𝐴 )
15	14	adantl	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴 ) → 𝑋 ⊆ 𝐴 )
16	1 2	atpsubN	⊢ ( 𝐾 ∈ 𝑉 → 𝐴 ∈ 𝑆 )
17	16	adantr	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴 ) → 𝐴 ∈ 𝑆 )
18		sseq2	⊢ ( 𝑦 = 𝐴 → ( 𝑋 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝐴 ) )
19	18	elrab3	⊢ ( 𝐴 ∈ 𝑆 → ( 𝐴 ∈ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ↔ 𝑋 ⊆ 𝐴 ) )
20	17 19	syl	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴 ) → ( 𝐴 ∈ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ↔ 𝑋 ⊆ 𝐴 ) )
21	15 20	mpbird	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴 ) → 𝐴 ∈ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )
22	21	ne0d	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴 ) → { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ≠ ∅ )
23		intex	⊢ ( { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ≠ ∅ ↔ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∈ V )
24	22 23	sylib	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴 ) → ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ∈ V )
25	9 12 13 24	fvmptd3	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴 ) → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦 } ) ‘ 𝑋 ) = ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )
26	8 25	eqtrd	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴 ) → ( 𝑈 ‘ 𝑋 ) = ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )
27	5 26	sylan2br	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) = ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )