tglndim0

Description: There are no lines in dimension 0. (Contributed by Thierry Arnoux, 18-Oct-2019)

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		tglndim0.d	$⊢ φ \to \|B\| = 1$
6	5	ad4antr	$⊢ ((((φ \land A \in ran L) \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \to \|B\| = 1$
7		simpllr	$⊢ ((((φ \land A \in ran L) \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \to x \in B$
8		simplr	$⊢ ((((φ \land A \in ran L) \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \to y \in B$
9	1 6 7 8	tgldim0eq	$⊢ ((((φ \land A \in ran L) \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \to x = y$
10		simprr	$⊢ ((((φ \land A \in ran L) \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \to x \neq y$
11	9 10	pm2.21ddne	$⊢ ((((φ \land A \in ran L) \land x \in B) \land y \in B) \land (A = x L y \land x \neq y)) \to ⊥$
12	4	adantr	$⊢ (φ \land A \in ran L) \to G \in 𝒢_{Tarski}$
13		simpr	$⊢ (φ \land A \in ran L) \to A \in ran L$
14	1 2 3 12 13	tgisline	$⊢ (φ \land A \in ran L) \to \exists x \in B \exists y \in B (A = x L y \land x \neq y)$
15	11 14	r19.29vva	$⊢ (φ \land A \in ran L) \to ⊥$
16	15	inegd	$⊢ φ \to \neg A \in ran L$

Metamath Proof Explorer