tghilberti2

Description: There is at most one line through any two distinct points. Hilbert's axiom I.2 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 = {Line}_{𝒢} (G)$
	tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	tglineelsb2.1	$⊢ φ \to P \in B$
	tglineelsb2.2	$⊢ φ \to Q \in B$
	tglineelsb2.4	$⊢ φ \to P \neq Q$
Assertion	tghilberti2	$⊢ φ \to \exists^{*} x \in ran L (P \in x \land Q \in x)$

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	$⊢ B = {Base}_{G}$
2		tglineelsb2.i	$⊢ I = Itv (G)$
3		tglineelsb2.l	$⊢ L = {Line}_{𝒢} (G)$
4		tglineelsb2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		tglineelsb2.1	$⊢ φ \to P \in B$
6		tglineelsb2.2	$⊢ φ \to Q \in B$
7		tglineelsb2.4	$⊢ φ \to P \neq Q$
8	4	3ad2ant1	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to G \in 𝒢_{Tarski}$
9	5	3ad2ant1	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to P \in B$
10	6	3ad2ant1	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to Q \in B$
11	7	3ad2ant1	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to P \neq Q$
12		simp2l	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to x \in ran L$
13		simp3ll	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to P \in x$
14		simp3lr	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to Q \in x$
15	1 2 3 8 9 10 11 11 12 13 14	tglinethru	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to x = P L Q$
16		simp2r	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to y \in ran L$
17		simp3rl	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to P \in y$
18		simp3rr	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to Q \in y$
19	1 2 3 8 9 10 11 11 16 17 18	tglinethru	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to y = P L Q$
20	15 19	eqtr4d	$⊢ (φ \land (x \in ran L \land y \in ran L) \land ((P \in x \land Q \in x) \land (P \in y \land Q \in y))) \to x = y$
21	20	3expia	$⊢ (φ \land (x \in ran L \land y \in ran L)) \to (((P \in x \land Q \in x) \land (P \in y \land Q \in y)) \to x = y)$
22	21	ralrimivva	$⊢ φ \to \forall x \in ran L \forall y \in ran L (((P \in x \land Q \in x) \land (P \in y \land Q \in y)) \to x = y)$
23		eleq2w	$⊢ x = y \to (P \in x \leftrightarrow P \in y)$
24		eleq2w	$⊢ x = y \to (Q \in x \leftrightarrow Q \in y)$
25	23 24	anbi12d	$⊢ x = y \to ((P \in x \land Q \in x) \leftrightarrow (P \in y \land Q \in y))$
26	25	rmo4	$⊢ \exists^{*} x \in ran L (P \in x \land Q \in x) \leftrightarrow \forall x \in ran L \forall y \in ran L (((P \in x \land Q \in x) \land (P \in y \land Q \in y)) \to x = y)$
27	22 26	sylibr	$⊢ φ \to \exists^{*} x \in ran L (P \in x \land Q \in x)$

Metamath Proof Explorer

Theorem tghilberti2

Proof