outsideofeu

Description: Given a nondegenerate ray, there is a unique point congruent to the segment B C lying on the ray A R . Theorem 6.11 of Schwabhauser p. 44. (Contributed by Scott Fenton, 23-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	outsideofeu	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((R \neq A \land B \neq C) \to \exists! x \in 𝔼 (N) (A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩))$

Proof

Step	Hyp	Ref	Expression
1		segcon2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to \exists x \in 𝔼 (N) ((R Btwn ⟨A, x⟩ \lor x Btwn ⟨A, R⟩) \land ⟨A, x⟩ Cgr ⟨B, C⟩)$
2	1	adantr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (R \neq A \land B \neq C)) \to \exists x \in 𝔼 (N) ((R Btwn ⟨A, x⟩ \lor x Btwn ⟨A, R⟩) \land ⟨A, x⟩ Cgr ⟨B, C⟩)$
3		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \to N \in ℕ$
4		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \to A \in 𝔼 (N)$
5		simpr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \to x \in 𝔼 (N)$
6		simpl2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \to R \in 𝔼 (N)$
7		broutsideof2	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land x \in 𝔼 (N) \land R \in 𝔼 (N))) \to (A OutsideOf ⟨x, R⟩ \leftrightarrow (x \neq A \land R \neq A \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩)))$
8	3 4 5 6 7	syl13anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (A OutsideOf ⟨x, R⟩ \leftrightarrow (x \neq A \land R \neq A \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩)))$
9	8	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩)) \to (A OutsideOf ⟨x, R⟩ \leftrightarrow (x \neq A \land R \neq A \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩)))$
10		simp3	$⊢ (x \neq A \land R \neq A \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩)) \to (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩)$
11		simpllr	$⊢ (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩)) \to B \neq C$
12	11	adantl	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))) \to B \neq C$
13		simprlr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))) \to ⟨A, x⟩ Cgr ⟨B, C⟩$
14		simp2l	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to A \in 𝔼 (N)$
15	14	anim1i	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (A \in 𝔼 (N) \land x \in 𝔼 (N))$
16		simpl3	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (B \in 𝔼 (N) \land C \in 𝔼 (N))$
17		cgrdegen	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land x \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to (⟨A, x⟩ Cgr ⟨B, C⟩ \to (A = x \leftrightarrow B = C))$
18	3 15 16 17	syl3anc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \to (⟨A, x⟩ Cgr ⟨B, C⟩ \to (A = x \leftrightarrow B = C))$
19	18	adantr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))) \to (⟨A, x⟩ Cgr ⟨B, C⟩ \to (A = x \leftrightarrow B = C))$
20	13 19	mpd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))) \to (A = x \leftrightarrow B = C)$
21	20	necon3bid	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))) \to (A \neq x \leftrightarrow B \neq C)$
22	12 21	mpbird	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))) \to A \neq x$
23	22	necomd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))) \to x \neq A$
24		simplll	$⊢ (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩)) \to R \neq A$
25	24	adantl	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))) \to R \neq A$
26		simprr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))) \to (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩)$
27	23 25 26	3jca	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))) \to (x \neq A \land R \neq A \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))$
28	27	expr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩)) \to ((x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩) \to (x \neq A \land R \neq A \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩)))$
29	10 28	impbid2	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩)) \to ((x \neq A \land R \neq A \land (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩)) \leftrightarrow (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))$
30	9 29	bitrd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩)) \to (A OutsideOf ⟨x, R⟩ \leftrightarrow (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩))$
31		orcom	$⊢ (x Btwn ⟨A, R⟩ \lor R Btwn ⟨A, x⟩) \leftrightarrow (R Btwn ⟨A, x⟩ \lor x Btwn ⟨A, R⟩)$
32	30 31	bitrdi	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land ((R \neq A \land B \neq C) \land ⟨A, x⟩ Cgr ⟨B, C⟩)) \to (A OutsideOf ⟨x, R⟩ \leftrightarrow (R Btwn ⟨A, x⟩ \lor x Btwn ⟨A, R⟩))$
33	32	expr	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (R \neq A \land B \neq C)) \to (⟨A, x⟩ Cgr ⟨B, C⟩ \to (A OutsideOf ⟨x, R⟩ \leftrightarrow (R Btwn ⟨A, x⟩ \lor x Btwn ⟨A, R⟩)))$
34	33	pm5.32rd	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land x \in 𝔼 (N)) \land (R \neq A \land B \neq C)) \to ((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \leftrightarrow ((R Btwn ⟨A, x⟩ \lor x Btwn ⟨A, R⟩) \land ⟨A, x⟩ Cgr ⟨B, C⟩))$
35	34	an32s	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (R \neq A \land B \neq C)) \land x \in 𝔼 (N)) \to ((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \leftrightarrow ((R Btwn ⟨A, x⟩ \lor x Btwn ⟨A, R⟩) \land ⟨A, x⟩ Cgr ⟨B, C⟩))$
36	35	rexbidva	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (R \neq A \land B \neq C)) \to (\exists x \in 𝔼 (N) (A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \leftrightarrow \exists x \in 𝔼 (N) ((R Btwn ⟨A, x⟩ \lor x Btwn ⟨A, R⟩) \land ⟨A, x⟩ Cgr ⟨B, C⟩))$
37	2 36	mpbird	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (R \neq A \land B \neq C)) \to \exists x \in 𝔼 (N) (A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩)$
38		simpl1	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \to N \in ℕ$
39		simpl2l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \to A \in 𝔼 (N)$
40		simpl2r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \to R \in 𝔼 (N)$
41		simpl3l	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \to B \in 𝔼 (N)$
42	39 40 41	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \to (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N))$
43		simpl3r	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \to C \in 𝔼 (N)$
44		simprl	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \to x \in 𝔼 (N)$
45		simprr	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \to y \in 𝔼 (N)$
46	43 44 45	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \to (C \in 𝔼 (N) \land x \in 𝔼 (N) \land y \in 𝔼 (N))$
47	38 42 46	3jca	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \to (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land x \in 𝔼 (N) \land y \in 𝔼 (N)))$
48		simpr	$⊢ ((R \neq A \land B \neq C) \land ((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨y, R⟩ \land ⟨A, y⟩ Cgr ⟨B, C⟩))) \to ((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨y, R⟩ \land ⟨A, y⟩ Cgr ⟨B, C⟩))$
49		outsideofeq	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land x \in 𝔼 (N) \land y \in 𝔼 (N))) \to (((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨y, R⟩ \land ⟨A, y⟩ Cgr ⟨B, C⟩)) \to x = y)$
50	49	imp	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N) \land B \in 𝔼 (N)) \land (C \in 𝔼 (N) \land x \in 𝔼 (N) \land y \in 𝔼 (N))) \land ((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨y, R⟩ \land ⟨A, y⟩ Cgr ⟨B, C⟩))) \to x = y$
51	47 48 50	syl2an	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (x \in 𝔼 (N) \land y \in 𝔼 (N))) \land ((R \neq A \land B \neq C) \land ((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨y, R⟩ \land ⟨A, y⟩ Cgr ⟨B, C⟩)))) \to x = y$
52	51	an4s	$⊢ (((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (R \neq A \land B \neq C)) \land ((x \in 𝔼 (N) \land y \in 𝔼 (N)) \land ((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨y, R⟩ \land ⟨A, y⟩ Cgr ⟨B, C⟩)))) \to x = y$
53	52	exp32	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (R \neq A \land B \neq C)) \to ((x \in 𝔼 (N) \land y \in 𝔼 (N)) \to (((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨y, R⟩ \land ⟨A, y⟩ Cgr ⟨B, C⟩)) \to x = y))$
54	53	ralrimivv	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (R \neq A \land B \neq C)) \to \forall x \in 𝔼 (N) \forall y \in 𝔼 (N) (((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨y, R⟩ \land ⟨A, y⟩ Cgr ⟨B, C⟩)) \to x = y)$
55		opeq1	$⊢ x = y \to ⟨x, R⟩ = ⟨y, R⟩$
56	55	breq2d	$⊢ x = y \to (A OutsideOf ⟨x, R⟩ \leftrightarrow A OutsideOf ⟨y, R⟩)$
57		opeq2	$⊢ x = y \to ⟨A, x⟩ = ⟨A, y⟩$
58	57	breq1d	$⊢ x = y \to (⟨A, x⟩ Cgr ⟨B, C⟩ \leftrightarrow ⟨A, y⟩ Cgr ⟨B, C⟩)$
59	56 58	anbi12d	$⊢ x = y \to ((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \leftrightarrow (A OutsideOf ⟨y, R⟩ \land ⟨A, y⟩ Cgr ⟨B, C⟩))$
60	59	reu4	$⊢ \exists! x \in 𝔼 (N) (A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \leftrightarrow (\exists x \in 𝔼 (N) (A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land \forall x \in 𝔼 (N) \forall y \in 𝔼 (N) (((A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩) \land (A OutsideOf ⟨y, R⟩ \land ⟨A, y⟩ Cgr ⟨B, C⟩)) \to x = y))$
61	37 54 60	sylanbrc	$⊢ ((N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \land (R \neq A \land B \neq C)) \to \exists! x \in 𝔼 (N) (A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩)$
62	61	ex	$⊢ (N \in ℕ \land (A \in 𝔼 (N) \land R \in 𝔼 (N)) \land (B \in 𝔼 (N) \land C \in 𝔼 (N))) \to ((R \neq A \land B \neq C) \to \exists! x \in 𝔼 (N) (A OutsideOf ⟨x, R⟩ \land ⟨A, x⟩ Cgr ⟨B, C⟩))$

Metamath Proof Explorer

Theorem outsideofeu

Proof