Theorem isline 33348

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

Hypotheses

Ref	Expression
isline.l	|- .<_ = ( le ` K )
isline.j	|- .\/ = ( join ` K )
isline.a	|- A = ( Atoms ` K )
isline.n	|- N = ( Lines ` K )

Assertion

Ref	Expression
isline	|- ( K e. D -> ( X e. N <-> E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) )

Distinct variable groups:   q, p, r, A   K, p, q, r   X, q, r

Allowed substitution hints:   D( r, q, p)   .\/ ( r, q, p)   .<_ ( r, q, p)   N( r, q, p)   X( p)

Proof of Theorem isline

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isline.l	. . . 4 |- .<_ = ( le ` K )
2		isline.j	. . . 4 |- .\/ = ( join ` K )
3		isline.a	. . . 4 |- A = ( Atoms ` K )
4		isline.n	. . . 4 |- N = ( Lines ` K )
5	1, 2, 3, 4	lineset 33347	. . 3 |- ( 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 2524	. 2 |- ( 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		fvex 5897	. . . . . . . . 9 |- ( Atoms ` K ) e. _V
8	3, 7	eqeltri 2535	. . . . . . . 8 |- A e. _V
9	8	rabex 4567	. . . . . . 7 |- { p e. A | p .<_ ( q .\/ r ) } e. _V
10		eleq1 2527	. . . . . . 7 |- ( X = { p e. A | p .<_ ( q .\/ r ) } -> ( X e. _V <-> { p e. A | p .<_ ( q .\/ r ) } e. _V ) )
11	9, 10	mpbiri 241	. . . . . 6 |- ( X = { p e. A | p .<_ ( q .\/ r ) } -> X e. _V )
12	11	adantl 472	. . . . 5 |- ( ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) -> X e. _V )
13	12	a1i 11	. . . 4 |- ( ( q e. A /\ r e. A ) -> ( ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) -> X e. _V ) )
14	13	rexlimivv 2895	. . 3 |- ( E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) -> X e. _V )
15		eqeq1 2465	. . . . 5 |- ( x = X -> ( x = { p e. A | p .<_ ( q .\/ r ) } <-> X = { p e. A | p .<_ ( q .\/ r ) } ) )
16	15	anbi2d 715	. . . 4 |- ( x = X -> ( ( q =/= r /\ x = { p e. A | p .<_ ( q .\/ r ) } ) <-> ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) )
17	16	2rexbidv 2919	. . 3 |- ( 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 ) } ) ) )
18	14, 17	elab3 3203	. 2 |- ( 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 ) } ) )
19	6, 18	syl6bb 269	1 |- ( K e. D -> ( X e. N <-> E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1454   e. wcel 1897   {cab 2447   =/= wne 2632   E.wrex 2749   {crab 2752   _Vcvv 3056   class class class wbr 4415   ` cfv 5600  (class class class)co 6314   lecple 15245   joincjn 16237   Atomscatm 32873   Linesclines 33103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pr 4652  ax-un 6609

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-uni 4212  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-ov 6317  df-lines 33110

This theorem is referenced by:  islinei  33349  linepsubN  33361  isline2  33383