ispsubclN

Description: The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	psubclset.a	$⊢ A = Atoms (K)$
	psubclset.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
	psubclset.c	$⊢ C = PSubCl (K)$
Assertion	ispsubclN	$⊢ K \in D \to (X \in C \leftrightarrow (X \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X))$

Step	Hyp	Ref	Expression
1		psubclset.a	$⊢ A = Atoms (K)$
2		psubclset.p	$⊢ \underset{˙}{⊥} = ⊥_{𝑃} (K)$
3		psubclset.c	$⊢ C = PSubCl (K)$
4	1 2 3	psubclsetN	$⊢ K \in D \to C = \{x \| (x \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)\}$
5	4	eleq2d	$⊢ K \in D \to (X \in C \leftrightarrow X \in \{x \| (x \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)\})$
6	1	fvexi	$⊢ A \in V$
7	6	ssex	$⊢ X \subseteq A \to X \in V$
8	7	adantr	$⊢ (X \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X) \to X \in V$
9		sseq1	$⊢ x = X \to (x \subseteq A \leftrightarrow X \subseteq A)$
10		2fveq3	$⊢ x = X \to \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = \underset{˙}{⊥} (\underset{˙}{⊥} (X))$
11		id	$⊢ x = X \to x = X$
12	10 11	eqeq12d	$⊢ x = X \to (\underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x \leftrightarrow \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)$
13	9 12	anbi12d	$⊢ x = X \to ((x \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x) \leftrightarrow (X \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X))$
14	8 13	elab3	$⊢ X \in \{x \| (x \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (x)) = x)\} \leftrightarrow (X \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X)$
15	5 14	bitrdi	$⊢ K \in D \to (X \in C \leftrightarrow (X \subseteq A \land \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = X))$

Metamath Proof Explorer