ispointN

Description: The predicate "is a point". (Contributed by NM, 2-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ispoint.a	$⊢ A = Atoms (K)$
	ispoint.p	$⊢ P = Points (K)$
Assertion	ispointN	$⊢ K \in D \to (X \in P \leftrightarrow \exists a \in A X = \{a\})$

Step	Hyp	Ref	Expression
1		ispoint.a	$⊢ A = Atoms (K)$
2		ispoint.p	$⊢ P = Points (K)$
3	1 2	pointsetN	$⊢ K \in D \to P = \{x \| \exists a \in A x = \{a\}\}$
4	3	eleq2d	$⊢ K \in D \to (X \in P \leftrightarrow X \in \{x \| \exists a \in A x = \{a\}\})$
5		vsnex	$⊢ \{a\} \in V$
6		eleq1	$⊢ X = \{a\} \to (X \in V \leftrightarrow \{a\} \in V)$
7	5 6	mpbiri	$⊢ X = \{a\} \to X \in V$
8	7	rexlimivw	$⊢ \exists a \in A X = \{a\} \to X \in V$
9		eqeq1	$⊢ x = X \to (x = \{a\} \leftrightarrow X = \{a\})$
10	9	rexbidv	$⊢ x = X \to (\exists a \in A x = \{a\} \leftrightarrow \exists a \in A X = \{a\})$
11	8 10	elab3	$⊢ X \in \{x \| \exists a \in A x = \{a\}\} \leftrightarrow \exists a \in A X = \{a\}$
12	4 11	bitrdi	$⊢ K \in D \to (X \in P \leftrightarrow \exists a \in A X = \{a\})$

Metamath Proof Explorer