Theorem tglnne0

Description: A line A has at least one point. (Contributed by Thierry Arnoux, 4-Mar-2020)

	Ref	Expression
Hypotheses	tglnne0.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	tglnne0.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tglnne0.1	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
Assertion	tglnne0	⊢ ( 𝜑 → 𝐴 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		tglnne0.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
2		tglnne0.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
3		tglnne0.1	⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5		eqid	⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
6	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐺 ∈ TarskiG )
7		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
8		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
9		simprr	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ≠ 𝑦 )
10	4 5 1 6 7 8 9	tglinerflx1	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ( 𝑥 𝐿 𝑦 ) )
11		simprl	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐴 = ( 𝑥 𝐿 𝑦 ) )
12	10 11	eleqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ 𝐴 )
13	12	ne0d	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝐴 ≠ ∅ )
14	4 5 1 2 3	tgisline	⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Base ‘ 𝐺 ) ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝐴 = ( 𝑥 𝐿 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
15	13 14	r19.29vva	⊢ ( 𝜑 → 𝐴 ≠ ∅ )