Theorem islln

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

	Ref	Expression
Hypotheses	llnset.b	|- B = ( Base ` K )
	llnset.c	|- C = (
	llnset.a	|- A = ( Atoms ` K )
	llnset.n	|- N = ( LLines ` K )
Assertion	islln	|- ( K e. D -> ( X e. N <-> ( X e. B /\ E. p e. A p C X ) ) )

Proof

Step	Hyp	Ref	Expression
1		llnset.b	|- B = ( Base ` K )
2		llnset.c	|- C = (
3		llnset.a	|- A = ( Atoms ` K )
4		llnset.n	|- N = ( LLines ` K )
5	1 2 3 4	llnset	|- ( K e. D -> N = { x e. B | E. p e. A p C x } )
6	5	eleq2d	|- ( K e. D -> ( X e. N <-> X e. { x e. B | E. p e. A p C x } ) )
7		breq2	|- ( x = X -> ( p C x <-> p C X ) )
8	7	rexbidv	|- ( x = X -> ( E. p e. A p C x <-> E. p e. A p C X ) )
9	8	elrab	|- ( X e. { x e. B | E. p e. A p C x } <-> ( X e. B /\ E. p e. A p C X ) )
10	6 9	bitrdi	|- ( K e. D -> ( X e. N <-> ( X e. B /\ E. p e. A p C X ) ) )