islpln

Description: The predicate "is a lattice plane". (Contributed by NM, 16-Jun-2012)

	Ref	Expression
Hypotheses	lplnset.b	$⊢ B = {Base}_{K}$
	lplnset.c	$⊢ C = ⋖_{K}$
	lplnset.n	$⊢ N = LLines (K)$
	lplnset.p	$⊢ P = LPlanes (K)$
Assertion	islpln	$⊢ K \in A \to (X \in P \leftrightarrow (X \in B \land \exists y \in N y C X))$

Step	Hyp	Ref	Expression
1		lplnset.b	$⊢ B = {Base}_{K}$
2		lplnset.c	$⊢ C = ⋖_{K}$
3		lplnset.n	$⊢ N = LLines (K)$
4		lplnset.p	$⊢ P = LPlanes (K)$
5	1 2 3 4	lplnset	$⊢ K \in A \to P = \{x \in B \| \exists y \in N y C x\}$
6	5	eleq2d	$⊢ K \in A \to (X \in P \leftrightarrow X \in \{x \in B \| \exists y \in N y C x\})$
7		breq2	$⊢ x = X \to (y C x \leftrightarrow y C X)$
8	7	rexbidv	$⊢ x = X \to (\exists y \in N y C x \leftrightarrow \exists y \in N y C X)$
9	8	elrab	$⊢ X \in \{x \in B \| \exists y \in N y C x\} \leftrightarrow (X \in B \land \exists y \in N y C X)$
10	6 9	bitrdi	$⊢ K \in A \to (X \in P \leftrightarrow (X \in B \land \exists y \in N y C X))$

Metamath Proof Explorer