oppnid

Description: The "opposite to a line" relation is irreflexive. (Contributed by Thierry Arnoux, 4-Mar-2020)

	Ref	Expression
Hypotheses	hpg.p	$⊢ P = {Base}_{G}$
	hpg.d	$⊢ \underset{˙}{-} = dist (G)$
	hpg.i	$⊢ I = Itv (G)$
	hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	opphl.l	$⊢ L = {Line}_{𝒢} (G)$
	opphl.d	$⊢ φ \to D \in ran L$
	opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	oppnid.1	$⊢ φ \to A \in P$
Assertion	oppnid	$⊢ φ \to \neg A O A$

Step	Hyp	Ref	Expression
1		hpg.p	$⊢ P = {Base}_{G}$
2		hpg.d	$⊢ \underset{˙}{-} = dist (G)$
3		hpg.i	$⊢ I = Itv (G)$
4		hpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		opphl.l	$⊢ L = {Line}_{𝒢} (G)$
6		opphl.d	$⊢ φ \to D \in ran L$
7		opphl.g	$⊢ φ \to G \in 𝒢_{Tarski}$
8		oppnid.1	$⊢ φ \to A \in P$
9	7	ad3antrrr	$⊢ (((φ \land A O A) \land t \in D) \land t \in (A I A)) \to G \in 𝒢_{Tarski}$
10	8	ad3antrrr	$⊢ (((φ \land A O A) \land t \in D) \land t \in (A I A)) \to A \in P$
11	6	ad3antrrr	$⊢ (((φ \land A O A) \land t \in D) \land t \in (A I A)) \to D \in ran L$
12		simplr	$⊢ (((φ \land A O A) \land t \in D) \land t \in (A I A)) \to t \in D$
13	1 5 3 9 11 12	tglnpt	$⊢ (((φ \land A O A) \land t \in D) \land t \in (A I A)) \to t \in P$
14		simpr	$⊢ (((φ \land A O A) \land t \in D) \land t \in (A I A)) \to t \in (A I A)$
15	1 2 3 9 10 13 14	axtgbtwnid	$⊢ (((φ \land A O A) \land t \in D) \land t \in (A I A)) \to A = t$
16	15 12	eqeltrd	$⊢ (((φ \land A O A) \land t \in D) \land t \in (A I A)) \to A \in D$
17	1 2 3 4 8 8	islnopp	$⊢ φ \to (A O A \leftrightarrow ((\neg A \in D \land \neg A \in D) \land \exists t \in D t \in (A I A)))$
18	17	simplbda	$⊢ (φ \land A O A) \to \exists t \in D t \in (A I A)$
19	16 18	r19.29a	$⊢ (φ \land A O A) \to A \in D$
20	17	simprbda	$⊢ (φ \land A O A) \to (\neg A \in D \land \neg A \in D)$
21	20	simpld	$⊢ (φ \land A O A) \to \neg A \in D$
22	19 21	pm2.65da	$⊢ φ \to \neg A O A$

Metamath Proof Explorer