Theorem tghilberti1

Description: There is a line through any two distinct points. Hilbert's axiom I.1 for geometry. (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	tghilberti1	|- ( ph -> E. x e. ran L ( P e. x /\ Q e. x ) )

Proof

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	tgelrnln	|- ( ph -> ( P L Q ) e. ran L )
9	1 2 3 4 5 6 7	tglinerflx1	|- ( ph -> P e. ( P L Q ) )
10	1 2 3 4 5 6 7	tglinerflx2	|- ( ph -> Q e. ( P L Q ) )
11		eleq2	|- ( x = ( P L Q ) -> ( P e. x <-> P e. ( P L Q ) ) )
12		eleq2	|- ( x = ( P L Q ) -> ( Q e. x <-> Q e. ( P L Q ) ) )
13	11 12	anbi12d	|- ( x = ( P L Q ) -> ( ( P e. x /\ Q e. x ) <-> ( P e. ( P L Q ) /\ Q e. ( P L Q ) ) ) )
14	13	rspcev	|- ( ( ( P L Q ) e. ran L /\ ( P e. ( P L Q ) /\ Q e. ( P L Q ) ) ) -> E. x e. ran L ( P e. x /\ Q e. x ) )
15	8 9 10 14	syl12anc	|- ( ph -> E. x e. ran L ( P e. x /\ Q e. x ) )