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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglineelsb2.1	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
	tglineelsb2.2	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
	tglineelsb2.4	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
Assertion	tghilberti2	⊢ ( 𝜑 → ∃* 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		tglineelsb2.p	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		tglineelsb2.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		tglineelsb2.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
4		tglineelsb2.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tglineelsb2.1	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
6		tglineelsb2.2	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
7		tglineelsb2.4	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
8	4	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝐺 ∈ TarskiG )
9	5	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑃 ∈ 𝐵 )
10	6	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑄 ∈ 𝐵 )
11	7	3ad2ant1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑃 ≠ 𝑄 )
12		simp2l	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑥 ∈ ran 𝐿 )
13		simp3ll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑃 ∈ 𝑥 )
14		simp3lr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑄 ∈ 𝑥 )
15	1 2 3 8 9 10 11 11 12 13 14	tglinethru	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑥 = ( 𝑃 𝐿 𝑄 ) )
16		simp2r	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑦 ∈ ran 𝐿 )
17		simp3rl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑃 ∈ 𝑦 )
18		simp3rr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑄 ∈ 𝑦 )
19	1 2 3 8 9 10 11 11 16 17 18	tglinethru	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑦 = ( 𝑃 𝐿 𝑄 ) )
20	15 19	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ∧ ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) ) → 𝑥 = 𝑦 )
21	20	3expia	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ran 𝐿 ∧ 𝑦 ∈ ran 𝐿 ) ) → ( ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) → 𝑥 = 𝑦 ) )
22	21	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐿 ∀ 𝑦 ∈ ran 𝐿 ( ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) → 𝑥 = 𝑦 ) )
23		eleq2w	⊢ ( 𝑥 = 𝑦 → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦 ) )
24		eleq2w	⊢ ( 𝑥 = 𝑦 → ( 𝑄 ∈ 𝑥 ↔ 𝑄 ∈ 𝑦 ) )
25	23 24	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ↔ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) )
26	25	rmo4	⊢ ( ∃* 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ↔ ∀ 𝑥 ∈ ran 𝐿 ∀ 𝑦 ∈ ran 𝐿 ( ( ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) ∧ ( 𝑃 ∈ 𝑦 ∧ 𝑄 ∈ 𝑦 ) ) → 𝑥 = 𝑦 ) )
27	22 26	sylibr	⊢ ( 𝜑 → ∃* 𝑥 ∈ ran 𝐿 ( 𝑃 ∈ 𝑥 ∧ 𝑄 ∈ 𝑥 ) )

Metamath Proof Explorer

Theorem tghilberti2

Proof