elpclN

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

	Ref	Expression
Hypotheses	pclfval.a	$⊢ A = Atoms (K)$
	pclfval.s	$⊢ S = PSubSp (K)$
	pclfval.c	$⊢ U = PCl (K)$
	elpcl.q	$⊢ Q \in V$
Assertion	elpclN	$⊢ (K \in V \land X \subseteq A) \to (Q \in U (X) \leftrightarrow \forall y \in S (X \subseteq y \to Q \in y))$

Step	Hyp	Ref	Expression
1		pclfval.a	$⊢ A = Atoms (K)$
2		pclfval.s	$⊢ S = PSubSp (K)$
3		pclfval.c	$⊢ U = PCl (K)$
4		elpcl.q	$⊢ Q \in V$
5	1 2 3	pclvalN	$⊢ (K \in V \land X \subseteq A) \to U (X) = ⋂ \{y \in S \| X \subseteq y\}$
6	5	eleq2d	$⊢ (K \in V \land X \subseteq A) \to (Q \in U (X) \leftrightarrow Q \in ⋂ \{y \in S \| X \subseteq y\})$
7	4	elintrab	$⊢ Q \in ⋂ \{y \in S \| X \subseteq y\} \leftrightarrow \forall y \in S (X \subseteq y \to Q \in y)$
8	6 7	bitrdi	$⊢ (K \in V \land X \subseteq A) \to (Q \in U (X) \leftrightarrow \forall y \in S (X \subseteq y \to Q \in y))$

Metamath Proof Explorer