Theorem isline

Description: The predicate "is a line". (Contributed by NM, 19-Sep-2011)

	Ref	Expression
Hypotheses	isline.l	|- .<_ = ( le ` K )
	isline.j	|- .\/ = ( join ` K )
	isline.a	|- A = ( Atoms ` K )
	isline.n	|- N = ( Lines ` K )
Assertion	isline	|- ( K e. D -> ( X e. N <-> E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		isline.l	|- .<_ = ( le ` K )
2		isline.j	|- .\/ = ( join ` K )
3		isline.a	|- A = ( Atoms ` K )
4		isline.n	|- N = ( Lines ` K )
5	1 2 3 4	lineset	|- ( K e. D -> N = { x | E. q e. A E. r e. A ( q =/= r /\ x = { p e. A | p .<_ ( q .\/ r ) } ) } )
6	5	eleq2d	|- ( K e. D -> ( X e. N <-> X e. { x | E. q e. A E. r e. A ( q =/= r /\ x = { p e. A | p .<_ ( q .\/ r ) } ) } ) )
7	3	fvexi	|- A e. _V
8	7	rabex	|- { p e. A | p .<_ ( q .\/ r ) } e. _V
9		eleq1	|- ( X = { p e. A | p .<_ ( q .\/ r ) } -> ( X e. _V <-> { p e. A | p .<_ ( q .\/ r ) } e. _V ) )
10	8 9	mpbiri	|- ( X = { p e. A | p .<_ ( q .\/ r ) } -> X e. _V )
11	10	adantl	|- ( ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) -> X e. _V )
12	11	a1i	|- ( ( q e. A /\ r e. A ) -> ( ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) -> X e. _V ) )
13	12	rexlimivv	|- ( E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) -> X e. _V )
14		eqeq1	|- ( x = X -> ( x = { p e. A | p .<_ ( q .\/ r ) } <-> X = { p e. A | p .<_ ( q .\/ r ) } ) )
15	14	anbi2d	|- ( x = X -> ( ( q =/= r /\ x = { p e. A | p .<_ ( q .\/ r ) } ) <-> ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) )
16	15	2rexbidv	|- ( x = X -> ( E. q e. A E. r e. A ( q =/= r /\ x = { p e. A | p .<_ ( q .\/ r ) } ) <-> E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) )
17	13 16	elab3	|- ( X e. { x | E. q e. A E. r e. A ( q =/= r /\ x = { p e. A | p .<_ ( q .\/ r ) } ) } <-> E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) )
18	6 17	bitrdi	|- ( K e. D -> ( X e. N <-> E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) )