Metamath Proof Explorer

Theorem pclfvalN

Description: The projective subspace closure function. (Contributed by NM, 7-Sep-2013) (New usage is discouraged.)

Ref Expression
Hypotheses pclfval.a ⊢ A = Atoms ⁡ K
pclfval.s ⊢ S = PSubSp ⁡ K
pclfval.c ⊢ U = PCl ⁡ K
Assertion pclfvalN ⊢ K ∈ V → U = x ∈ 𝒫 A ⟼ ⋂ y ∈ S | x ⊆ y

Proof

Step Hyp Ref Expression
1 pclfval.a ⊢ A = Atoms ⁡ K
2 pclfval.s ⊢ S = PSubSp ⁡ K
3 pclfval.c ⊢ U = PCl ⁡ K
4 elex ⊢ K ∈ V → K ∈ V
5 fveq2 ⊢ k = K → Atoms ⁡ k = Atoms ⁡ K
6 5 1 eqtr4di ⊢ k = K → Atoms ⁡ k = A
7 6 pweqd ⊢ k = K → 𝒫 Atoms ⁡ k = 𝒫 A
8 fveq2 ⊢ k = K → PSubSp ⁡ k = PSubSp ⁡ K
9 8 2 eqtr4di ⊢ k = K → PSubSp ⁡ k = S
10 9 rabeqdv ⊢ k = K → y ∈ PSubSp ⁡ k | x ⊆ y = y ∈ S | x ⊆ y
11 10 inteqd ⊢ k = K → ⋂ y ∈ PSubSp ⁡ k | x ⊆ y = ⋂ y ∈ S | x ⊆ y
12 7 11 mpteq12dv ⊢ k = K → x ∈ 𝒫 Atoms ⁡ k ⟼ ⋂ y ∈ PSubSp ⁡ k | x ⊆ y = x ∈ 𝒫 A ⟼ ⋂ y ∈ S | x ⊆ y
13 df-pclN ⊢ PCl = k ∈ V ⟼ x ∈ 𝒫 Atoms ⁡ k ⟼ ⋂ y ∈ PSubSp ⁡ k | x ⊆ y
14 1 fvexi ⊢ A ∈ V
15 14 pwex ⊢ 𝒫 A ∈ V
16 15 mptex ⊢ x ∈ 𝒫 A ⟼ ⋂ y ∈ S | x ⊆ y ∈ V
17 12 13 16 fvmpt ⊢ K ∈ V → PCl ⁡ K = x ∈ 𝒫 A ⟼ ⋂ y ∈ S | x ⊆ y
18 3 17 syl5eq ⊢ K ∈ V → U = x ∈ 𝒫 A ⟼ ⋂ y ∈ S | x ⊆ y
19 4 18 syl ⊢ K ∈ V → U = x ∈ 𝒫 A ⟼ ⋂ y ∈ S | x ⊆ y