This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) } ) ) )