Theorem elpclN

Description: Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pclfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	pclfval.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
	pclfval.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
	elpcl.q	⊢ 𝑄 ∈ V
Assertion	elpclN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑄 ∈ ( 𝑈 ‘ 𝑋 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑄 ∈ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pclfval.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		pclfval.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
3		pclfval.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
4		elpcl.q	⊢ 𝑄 ∈ V
5	1 2 3	pclvalN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ 𝑋 ) = ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } )
6	5	eleq2d	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑄 ∈ ( 𝑈 ‘ 𝑋 ) ↔ 𝑄 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ) )
7	4	elintrab	⊢ ( 𝑄 ∈ ∩ { 𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦 } ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑄 ∈ 𝑦 ) )
8	6 7	bitrdi	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑄 ∈ ( 𝑈 ‘ 𝑋 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑋 ⊆ 𝑦 → 𝑄 ∈ 𝑦 ) ) )