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

Metamath Proof Explorer

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