Theorem elpcliN

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

	Ref	Expression
Hypotheses	elpcli.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
	elpcli.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
Assertion	elpcliN	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) ∧ 𝑄 ∈ ( 𝑈 ‘ 𝑋 ) ) → 𝑄 ∈ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		elpcli.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
2		elpcli.c	⊢ 𝑈 = ( PCl ‘ 𝐾 )
3		simp1	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) → 𝐾 ∈ 𝑉 )
4		simp2	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ⊆ 𝑌 )
5		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
6	5 1	psubssat	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
7	6	3adant2	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) → 𝑌 ⊆ ( Atoms ‘ 𝐾 ) )
8	4 7	sstrd	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) → 𝑋 ⊆ ( Atoms ‘ 𝐾 ) )
9	5 1 2	pclvalN	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ ( Atoms ‘ 𝐾 ) ) → ( 𝑈 ‘ 𝑋 ) = ∩ { 𝑧 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑧 } )
10	3 8 9	syl2anc	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑈 ‘ 𝑋 ) = ∩ { 𝑧 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑧 } )
11	10	eleq2d	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑄 ∈ ( 𝑈 ‘ 𝑋 ) ↔ 𝑄 ∈ ∩ { 𝑧 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑧 } ) )
12		elintrabg	⊢ ( 𝑄 ∈ ∩ { 𝑧 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑧 } → ( 𝑄 ∈ ∩ { 𝑧 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑧 } ↔ ∀ 𝑧 ∈ 𝑆 ( 𝑋 ⊆ 𝑧 → 𝑄 ∈ 𝑧 ) ) )
13	12	ibi	⊢ ( 𝑄 ∈ ∩ { 𝑧 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑧 } → ∀ 𝑧 ∈ 𝑆 ( 𝑋 ⊆ 𝑧 → 𝑄 ∈ 𝑧 ) )
14	11 13	syl6bi	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑄 ∈ ( 𝑈 ‘ 𝑋 ) → ∀ 𝑧 ∈ 𝑆 ( 𝑋 ⊆ 𝑧 → 𝑄 ∈ 𝑧 ) ) )
15		sseq2	⊢ ( 𝑧 = 𝑌 → ( 𝑋 ⊆ 𝑧 ↔ 𝑋 ⊆ 𝑌 ) )
16		eleq2	⊢ ( 𝑧 = 𝑌 → ( 𝑄 ∈ 𝑧 ↔ 𝑄 ∈ 𝑌 ) )
17	15 16	imbi12d	⊢ ( 𝑧 = 𝑌 → ( ( 𝑋 ⊆ 𝑧 → 𝑄 ∈ 𝑧 ) ↔ ( 𝑋 ⊆ 𝑌 → 𝑄 ∈ 𝑌 ) ) )
18	17	rspccv	⊢ ( ∀ 𝑧 ∈ 𝑆 ( 𝑋 ⊆ 𝑧 → 𝑄 ∈ 𝑧 ) → ( 𝑌 ∈ 𝑆 → ( 𝑋 ⊆ 𝑌 → 𝑄 ∈ 𝑌 ) ) )
19	18	com13	⊢ ( 𝑋 ⊆ 𝑌 → ( 𝑌 ∈ 𝑆 → ( ∀ 𝑧 ∈ 𝑆 ( 𝑋 ⊆ 𝑧 → 𝑄 ∈ 𝑧 ) → 𝑄 ∈ 𝑌 ) ) )
20	19	imp	⊢ ( ( 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) → ( ∀ 𝑧 ∈ 𝑆 ( 𝑋 ⊆ 𝑧 → 𝑄 ∈ 𝑧 ) → 𝑄 ∈ 𝑌 ) )
21	20	3adant1	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) → ( ∀ 𝑧 ∈ 𝑆 ( 𝑋 ⊆ 𝑧 → 𝑄 ∈ 𝑧 ) → 𝑄 ∈ 𝑌 ) )
22	14 21	syld	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑄 ∈ ( 𝑈 ‘ 𝑋 ) → 𝑄 ∈ 𝑌 ) )
23	22	imp	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆 ) ∧ 𝑄 ∈ ( 𝑈 ‘ 𝑋 ) ) → 𝑄 ∈ 𝑌 )