brcolinear2

Description: Alternate colinearity binary relation. (Contributed by Scott Fenton, 7-Nov-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	brcolinear2	$⊢ (Q \in V \land R \in W) \to (P Colinear ⟨Q, R⟩ \leftrightarrow \exists n \in ℕ ((P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩)))$

Proof

Step	Hyp	Ref	Expression
1		colinrel	$⊢ Rel Colinear$
2	1	brrelex1i	$⊢ P Colinear ⟨Q, R⟩ \to P \in V$
3	2	a1i	$⊢ (Q \in V \land R \in W) \to (P Colinear ⟨Q, R⟩ \to P \in V)$
4		elex	$⊢ P \in 𝔼 (n) \to P \in V$
5	4	3ad2ant1	$⊢ (P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \to P \in V$
6	5	adantr	$⊢ ((P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩)) \to P \in V$
7	6	rexlimivw	$⊢ \exists n \in ℕ ((P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩)) \to P \in V$
8	7	a1i	$⊢ (Q \in V \land R \in W) \to (\exists n \in ℕ ((P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩)) \to P \in V)$
9		df-br	$⊢ P Colinear ⟨Q, R⟩ \leftrightarrow ⟨P, ⟨Q, R⟩⟩ \in Colinear$
10		df-colinear	$⊢ Colinear = {\{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\}}^{-1}$
11	10	eleq2i	$⊢ ⟨P, ⟨Q, R⟩⟩ \in Colinear \leftrightarrow ⟨P, ⟨Q, R⟩⟩ \in {\{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\}}^{-1}$
12	9 11	bitri	$⊢ P Colinear ⟨Q, R⟩ \leftrightarrow ⟨P, ⟨Q, R⟩⟩ \in {\{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\}}^{-1}$
13		opex	$⊢ ⟨Q, R⟩ \in V$
14		opelcnvg	$⊢ (P \in V \land ⟨Q, R⟩ \in V) \to (⟨P, ⟨Q, R⟩⟩ \in {\{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\}}^{-1} \leftrightarrow ⟨⟨Q, R⟩, P⟩ \in \{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\})$
15	13 14	mpan2	$⊢ P \in V \to (⟨P, ⟨Q, R⟩⟩ \in {\{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\}}^{-1} \leftrightarrow ⟨⟨Q, R⟩, P⟩ \in \{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\})$
16	15	3ad2ant3	$⊢ (Q \in V \land R \in W \land P \in V) \to (⟨P, ⟨Q, R⟩⟩ \in {\{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\}}^{-1} \leftrightarrow ⟨⟨Q, R⟩, P⟩ \in \{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\})$
17	12 16	syl5bb	$⊢ (Q \in V \land R \in W \land P \in V) \to (P Colinear ⟨Q, R⟩ \leftrightarrow ⟨⟨Q, R⟩, P⟩ \in \{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\})$
18		eleq1	$⊢ q = Q \to (q \in 𝔼 (n) \leftrightarrow Q \in 𝔼 (n))$
19	18	3anbi2d	$⊢ q = Q \to ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \leftrightarrow (p \in 𝔼 (n) \land Q \in 𝔼 (n) \land r \in 𝔼 (n)))$
20		opeq1	$⊢ q = Q \to ⟨q, r⟩ = ⟨Q, r⟩$
21	20	breq2d	$⊢ q = Q \to (p Btwn ⟨q, r⟩ \leftrightarrow p Btwn ⟨Q, r⟩)$
22		breq1	$⊢ q = Q \to (q Btwn ⟨r, p⟩ \leftrightarrow Q Btwn ⟨r, p⟩)$
23		opeq2	$⊢ q = Q \to ⟨p, q⟩ = ⟨p, Q⟩$
24	23	breq2d	$⊢ q = Q \to (r Btwn ⟨p, q⟩ \leftrightarrow r Btwn ⟨p, Q⟩)$
25	21 22 24	3orbi123d	$⊢ q = Q \to ((p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩) \leftrightarrow (p Btwn ⟨Q, r⟩ \lor Q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, Q⟩))$
26	19 25	anbi12d	$⊢ q = Q \to (((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩)) \leftrightarrow ((p \in 𝔼 (n) \land Q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨Q, r⟩ \lor Q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, Q⟩)))$
27	26	rexbidv	$⊢ q = Q \to (\exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩)) \leftrightarrow \exists n \in ℕ ((p \in 𝔼 (n) \land Q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨Q, r⟩ \lor Q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, Q⟩)))$
28		eleq1	$⊢ r = R \to (r \in 𝔼 (n) \leftrightarrow R \in 𝔼 (n))$
29	28	3anbi3d	$⊢ r = R \to ((p \in 𝔼 (n) \land Q \in 𝔼 (n) \land r \in 𝔼 (n)) \leftrightarrow (p \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)))$
30		opeq2	$⊢ r = R \to ⟨Q, r⟩ = ⟨Q, R⟩$
31	30	breq2d	$⊢ r = R \to (p Btwn ⟨Q, r⟩ \leftrightarrow p Btwn ⟨Q, R⟩)$
32		opeq1	$⊢ r = R \to ⟨r, p⟩ = ⟨R, p⟩$
33	32	breq2d	$⊢ r = R \to (Q Btwn ⟨r, p⟩ \leftrightarrow Q Btwn ⟨R, p⟩)$
34		breq1	$⊢ r = R \to (r Btwn ⟨p, Q⟩ \leftrightarrow R Btwn ⟨p, Q⟩)$
35	31 33 34	3orbi123d	$⊢ r = R \to ((p Btwn ⟨Q, r⟩ \lor Q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, Q⟩) \leftrightarrow (p Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, p⟩ \lor R Btwn ⟨p, Q⟩))$
36	29 35	anbi12d	$⊢ r = R \to (((p \in 𝔼 (n) \land Q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨Q, r⟩ \lor Q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, Q⟩)) \leftrightarrow ((p \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (p Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, p⟩ \lor R Btwn ⟨p, Q⟩)))$
37	36	rexbidv	$⊢ r = R \to (\exists n \in ℕ ((p \in 𝔼 (n) \land Q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨Q, r⟩ \lor Q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, Q⟩)) \leftrightarrow \exists n \in ℕ ((p \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (p Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, p⟩ \lor R Btwn ⟨p, Q⟩)))$
38		eleq1	$⊢ p = P \to (p \in 𝔼 (n) \leftrightarrow P \in 𝔼 (n))$
39	38	3anbi1d	$⊢ p = P \to ((p \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \leftrightarrow (P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)))$
40		breq1	$⊢ p = P \to (p Btwn ⟨Q, R⟩ \leftrightarrow P Btwn ⟨Q, R⟩)$
41		opeq2	$⊢ p = P \to ⟨R, p⟩ = ⟨R, P⟩$
42	41	breq2d	$⊢ p = P \to (Q Btwn ⟨R, p⟩ \leftrightarrow Q Btwn ⟨R, P⟩)$
43		opeq1	$⊢ p = P \to ⟨p, Q⟩ = ⟨P, Q⟩$
44	43	breq2d	$⊢ p = P \to (R Btwn ⟨p, Q⟩ \leftrightarrow R Btwn ⟨P, Q⟩)$
45	40 42 44	3orbi123d	$⊢ p = P \to ((p Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, p⟩ \lor R Btwn ⟨p, Q⟩) \leftrightarrow (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩))$
46	39 45	anbi12d	$⊢ p = P \to (((p \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (p Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, p⟩ \lor R Btwn ⟨p, Q⟩)) \leftrightarrow ((P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩)))$
47	46	rexbidv	$⊢ p = P \to (\exists n \in ℕ ((p \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (p Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, p⟩ \lor R Btwn ⟨p, Q⟩)) \leftrightarrow \exists n \in ℕ ((P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩)))$
48	27 37 47	eloprabg	$⊢ (Q \in V \land R \in W \land P \in V) \to (⟨⟨Q, R⟩, P⟩ \in \{⟨⟨q, r⟩, p⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land r \in 𝔼 (n)) \land (p Btwn ⟨q, r⟩ \lor q Btwn ⟨r, p⟩ \lor r Btwn ⟨p, q⟩))\} \leftrightarrow \exists n \in ℕ ((P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩)))$
49	17 48	bitrd	$⊢ (Q \in V \land R \in W \land P \in V) \to (P Colinear ⟨Q, R⟩ \leftrightarrow \exists n \in ℕ ((P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩)))$
50	49	3expia	$⊢ (Q \in V \land R \in W) \to (P \in V \to (P Colinear ⟨Q, R⟩ \leftrightarrow \exists n \in ℕ ((P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩))))$
51	3 8 50	pm5.21ndd	$⊢ (Q \in V \land R \in W) \to (P Colinear ⟨Q, R⟩ \leftrightarrow \exists n \in ℕ ((P \in 𝔼 (n) \land Q \in 𝔼 (n) \land R \in 𝔼 (n)) \land (P Btwn ⟨Q, R⟩ \lor Q Btwn ⟨R, P⟩ \lor R Btwn ⟨P, Q⟩)))$

Metamath Proof Explorer

Theorem brcolinear2

Proof