tglnne0

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

Step	Hyp	Ref	Expression
1		tglnne0.l	$⊢ L = {Line}_{𝒢} (G)$
2		tglnne0.g	$⊢ φ \to G \in 𝒢_{Tarski}$
3		tglnne0.1	$⊢ φ \to A \in ran L$
4		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5		eqid	$⊢ Itv (G) = Itv (G)$
6	2	ad3antrrr	$⊢ (((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land (A = x L y \land x \neq y)) \to G \in 𝒢_{Tarski}$
7		simpllr	$⊢ (((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land (A = x L y \land x \neq y)) \to x \in {Base}_{G}$
8		simplr	$⊢ (((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land (A = x L y \land x \neq y)) \to y \in {Base}_{G}$
9		simprr	$⊢ (((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land (A = x L y \land x \neq y)) \to x \neq y$
10	4 5 1 6 7 8 9	tglinerflx1	$⊢ (((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land (A = x L y \land x \neq y)) \to x \in (x L y)$
11		simprl	$⊢ (((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land (A = x L y \land x \neq y)) \to A = x L y$
12	10 11	eleqtrrd	$⊢ (((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land (A = x L y \land x \neq y)) \to x \in A$
13	12	ne0d	$⊢ (((φ \land x \in {Base}_{G}) \land y \in {Base}_{G}) \land (A = x L y \land x \neq y)) \to A \neq \emptyset$
14	4 5 1 2 3	tgisline	$⊢ φ \to \exists x \in {Base}_{G} \exists y \in {Base}_{G} (A = x L y \land x \neq y)$
15	13 14	r19.29vva	$⊢ φ \to A \neq \emptyset$

Metamath Proof Explorer