Description: There is a unique line going through any two distinct points. Theorem 6.19 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 25-May-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | tglineelsb2.p | |- B = ( Base ` G ) |
|
| tglineelsb2.i | |- I = ( Itv ` G ) |
||
| tglineelsb2.l | |- L = ( LineG ` G ) |
||
| tglineelsb2.g | |- ( ph -> G e. TarskiG ) |
||
| tglineelsb2.1 | |- ( ph -> P e. B ) |
||
| tglineelsb2.2 | |- ( ph -> Q e. B ) |
||
| tglineelsb2.4 | |- ( ph -> P =/= Q ) |
||
| Assertion | tglinethrueu | |- ( ph -> E! x e. ran L ( P e. x /\ Q e. x ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tglineelsb2.p | |- B = ( Base ` G ) |
|
| 2 | tglineelsb2.i | |- I = ( Itv ` G ) |
|
| 3 | tglineelsb2.l | |- L = ( LineG ` G ) |
|
| 4 | tglineelsb2.g | |- ( ph -> G e. TarskiG ) |
|
| 5 | tglineelsb2.1 | |- ( ph -> P e. B ) |
|
| 6 | tglineelsb2.2 | |- ( ph -> Q e. B ) |
|
| 7 | tglineelsb2.4 | |- ( ph -> P =/= Q ) |
|
| 8 | 1 2 3 4 5 6 7 | tghilberti1 | |- ( ph -> E. x e. ran L ( P e. x /\ Q e. x ) ) |
| 9 | 1 2 3 4 5 6 7 | tghilberti2 | |- ( ph -> E* x e. ran L ( P e. x /\ Q e. x ) ) |
| 10 | reu5 | |- ( E! x e. ran L ( P e. x /\ Q e. x ) <-> ( E. x e. ran L ( P e. x /\ Q e. x ) /\ E* x e. ran L ( P e. x /\ Q e. x ) ) ) |
|
| 11 | 8 9 10 | sylanbrc | |- ( ph -> E! x e. ran L ( P e. x /\ Q e. x ) ) |