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 \in V \to U = (x \in 𝒫 A ⟼ ⋂ \{y \in S \| x \subseteq y\})$

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 \in V \to K \in V$
5		fveq2	$⊢ k = K \to Atoms (k) = Atoms (K)$
6	5 1	eqtr4di	$⊢ k = K \to Atoms (k) = A$
7	6	pweqd	$⊢ k = K \to 𝒫 Atoms (k) = 𝒫 A$
8		fveq2	$⊢ k = K \to PSubSp (k) = PSubSp (K)$
9	8 2	eqtr4di	$⊢ k = K \to PSubSp (k) = S$
10	9	rabeqdv	$⊢ k = K \to \{y \in PSubSp (k) \| x \subseteq y\} = \{y \in S \| x \subseteq y\}$
11	10	inteqd	$⊢ k = K \to ⋂ \{y \in PSubSp (k) \| x \subseteq y\} = ⋂ \{y \in S \| x \subseteq y\}$
12	7 11	mpteq12dv	$⊢ k = K \to (x \in 𝒫 Atoms (k) ⟼ ⋂ \{y \in PSubSp (k) \| x \subseteq y\}) = (x \in 𝒫 A ⟼ ⋂ \{y \in S \| x \subseteq y\})$
13		df-pclN	$⊢ PCl = (k \in V ⟼ (x \in 𝒫 Atoms (k) ⟼ ⋂ \{y \in PSubSp (k) \| x \subseteq y\}))$
14	1	fvexi	$⊢ A \in V$
15	14	pwex	$⊢ 𝒫 A \in V$
16	15	mptex	$⊢ (x \in 𝒫 A ⟼ ⋂ \{y \in S \| x \subseteq y\}) \in V$
17	12 13 16	fvmpt	$⊢ K \in V \to PCl (K) = (x \in 𝒫 A ⟼ ⋂ \{y \in S \| x \subseteq y\})$
18	3 17	eqtrid	$⊢ K \in V \to U = (x \in 𝒫 A ⟼ ⋂ \{y \in S \| x \subseteq y\})$
19	4 18	syl	$⊢ K \in V \to U = (x \in 𝒫 A ⟼ ⋂ \{y \in S \| x \subseteq y\})$

Metamath Proof Explorer