Metamath Proof Explorer


Theorem isline

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

Ref Expression
Hypotheses isline.l ˙ = K
isline.j ˙ = join K
isline.a A = Atoms K
isline.n N = Lines K
Assertion isline K D X N q A r A q r X = p A | p ˙ q ˙ r

Proof

Step Hyp Ref Expression
1 isline.l ˙ = 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 D N = x | q A r A q r x = p A | p ˙ q ˙ r
6 5 eleq2d K D X N X x | q A r A q r x = p A | p ˙ q ˙ r
7 3 fvexi A V
8 7 rabex p A | p ˙ q ˙ r V
9 eleq1 X = p A | p ˙ q ˙ r X V p A | p ˙ q ˙ r V
10 8 9 mpbiri X = p A | p ˙ q ˙ r X V
11 10 adantl q r X = p A | p ˙ q ˙ r X V
12 11 a1i q A r A q r X = p A | p ˙ q ˙ r X V
13 12 rexlimivv q A r A q r X = p A | p ˙ q ˙ r X V
14 eqeq1 x = X x = p A | p ˙ q ˙ r X = p A | p ˙ q ˙ r
15 14 anbi2d x = X q r x = p A | p ˙ q ˙ r q r X = p A | p ˙ q ˙ r
16 15 2rexbidv x = X q A r A q r x = p A | p ˙ q ˙ r q A r A q r X = p A | p ˙ q ˙ r
17 13 16 elab3 X x | q A r A q r x = p A | p ˙ q ˙ r q A r A q r X = p A | p ˙ q ˙ r
18 6 17 bitrdi K D X N q A r A q r X = p A | p ˙ q ˙ r