Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brcolinear2 Structured version   Visualization version   GIF version

Theorem brcolinear2 34360
Description: Alternate colinearity binary relation. (Contributed by Scott Fenton, 7-Nov-2013.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
brcolinear2 ((𝑄𝑉𝑅𝑊) → (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
Distinct variable groups:   𝑃,𝑛   𝑄,𝑛   𝑅,𝑛
Allowed substitution hints:   𝑉(𝑛)   𝑊(𝑛)

Proof of Theorem brcolinear2
Dummy variables 𝑝 𝑞 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 colinrel 34359 . . . 4 Rel Colinear
21brrelex1i 5643 . . 3 (𝑃 Colinear ⟨𝑄, 𝑅⟩ → 𝑃 ∈ V)
32a1i 11 . 2 ((𝑄𝑉𝑅𝑊) → (𝑃 Colinear ⟨𝑄, 𝑅⟩ → 𝑃 ∈ V))
4 elex 3450 . . . . . 6 (𝑃 ∈ (𝔼‘𝑛) → 𝑃 ∈ V)
543ad2ant1 1132 . . . . 5 ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) → 𝑃 ∈ V)
65adantr 481 . . . 4 (((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 ∈ V)
76rexlimivw 3211 . . 3 (∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 ∈ V)
87a1i 11 . 2 ((𝑄𝑉𝑅𝑊) → (∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 ∈ V))
9 df-br 5075 . . . . . 6 (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ Colinear )
10 df-colinear 34341 . . . . . . 7 Colinear = {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))}
1110eleq2i 2830 . . . . . 6 (⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ Colinear ↔ ⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))})
129, 11bitri 274 . . . . 5 (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))})
13 opex 5379 . . . . . . 7 𝑄, 𝑅⟩ ∈ V
14 opelcnvg 5789 . . . . . . 7 ((𝑃 ∈ V ∧ ⟨𝑄, 𝑅⟩ ∈ V) → (⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))} ↔ ⟨⟨𝑄, 𝑅⟩, 𝑃⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))}))
1513, 14mpan2 688 . . . . . 6 (𝑃 ∈ V → (⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))} ↔ ⟨⟨𝑄, 𝑅⟩, 𝑃⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))}))
16153ad2ant3 1134 . . . . 5 ((𝑄𝑉𝑅𝑊𝑃 ∈ V) → (⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))} ↔ ⟨⟨𝑄, 𝑅⟩, 𝑃⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))}))
1712, 16syl5bb 283 . . . 4 ((𝑄𝑉𝑅𝑊𝑃 ∈ V) → (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ⟨⟨𝑄, 𝑅⟩, 𝑃⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))}))
18 eleq1 2826 . . . . . . . 8 (𝑞 = 𝑄 → (𝑞 ∈ (𝔼‘𝑛) ↔ 𝑄 ∈ (𝔼‘𝑛)))
19183anbi2d 1440 . . . . . . 7 (𝑞 = 𝑄 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ↔ (𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛))))
20 opeq1 4804 . . . . . . . . 9 (𝑞 = 𝑄 → ⟨𝑞, 𝑟⟩ = ⟨𝑄, 𝑟⟩)
2120breq2d 5086 . . . . . . . 8 (𝑞 = 𝑄 → (𝑝 Btwn ⟨𝑞, 𝑟⟩ ↔ 𝑝 Btwn ⟨𝑄, 𝑟⟩))
22 breq1 5077 . . . . . . . 8 (𝑞 = 𝑄 → (𝑞 Btwn ⟨𝑟, 𝑝⟩ ↔ 𝑄 Btwn ⟨𝑟, 𝑝⟩))
23 opeq2 4805 . . . . . . . . 9 (𝑞 = 𝑄 → ⟨𝑝, 𝑞⟩ = ⟨𝑝, 𝑄⟩)
2423breq2d 5086 . . . . . . . 8 (𝑞 = 𝑄 → (𝑟 Btwn ⟨𝑝, 𝑞⟩ ↔ 𝑟 Btwn ⟨𝑝, 𝑄⟩))
2521, 22, 243orbi123d 1434 . . . . . . 7 (𝑞 = 𝑄 → ((𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩) ↔ (𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩)))
2619, 25anbi12d 631 . . . . . 6 (𝑞 = 𝑄 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩)) ↔ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩))))
2726rexbidv 3226 . . . . 5 (𝑞 = 𝑄 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩)) ↔ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩))))
28 eleq1 2826 . . . . . . . 8 (𝑟 = 𝑅 → (𝑟 ∈ (𝔼‘𝑛) ↔ 𝑅 ∈ (𝔼‘𝑛)))
29283anbi3d 1441 . . . . . . 7 (𝑟 = 𝑅 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ↔ (𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛))))
30 opeq2 4805 . . . . . . . . 9 (𝑟 = 𝑅 → ⟨𝑄, 𝑟⟩ = ⟨𝑄, 𝑅⟩)
3130breq2d 5086 . . . . . . . 8 (𝑟 = 𝑅 → (𝑝 Btwn ⟨𝑄, 𝑟⟩ ↔ 𝑝 Btwn ⟨𝑄, 𝑅⟩))
32 opeq1 4804 . . . . . . . . 9 (𝑟 = 𝑅 → ⟨𝑟, 𝑝⟩ = ⟨𝑅, 𝑝⟩)
3332breq2d 5086 . . . . . . . 8 (𝑟 = 𝑅 → (𝑄 Btwn ⟨𝑟, 𝑝⟩ ↔ 𝑄 Btwn ⟨𝑅, 𝑝⟩))
34 breq1 5077 . . . . . . . 8 (𝑟 = 𝑅 → (𝑟 Btwn ⟨𝑝, 𝑄⟩ ↔ 𝑅 Btwn ⟨𝑝, 𝑄⟩))
3531, 33, 343orbi123d 1434 . . . . . . 7 (𝑟 = 𝑅 → ((𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩) ↔ (𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩)))
3629, 35anbi12d 631 . . . . . 6 (𝑟 = 𝑅 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩)) ↔ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩))))
3736rexbidv 3226 . . . . 5 (𝑟 = 𝑅 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩)) ↔ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩))))
38 eleq1 2826 . . . . . . . 8 (𝑝 = 𝑃 → (𝑝 ∈ (𝔼‘𝑛) ↔ 𝑃 ∈ (𝔼‘𝑛)))
39383anbi1d 1439 . . . . . . 7 (𝑝 = 𝑃 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ↔ (𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛))))
40 breq1 5077 . . . . . . . 8 (𝑝 = 𝑃 → (𝑝 Btwn ⟨𝑄, 𝑅⟩ ↔ 𝑃 Btwn ⟨𝑄, 𝑅⟩))
41 opeq2 4805 . . . . . . . . 9 (𝑝 = 𝑃 → ⟨𝑅, 𝑝⟩ = ⟨𝑅, 𝑃⟩)
4241breq2d 5086 . . . . . . . 8 (𝑝 = 𝑃 → (𝑄 Btwn ⟨𝑅, 𝑝⟩ ↔ 𝑄 Btwn ⟨𝑅, 𝑃⟩))
43 opeq1 4804 . . . . . . . . 9 (𝑝 = 𝑃 → ⟨𝑝, 𝑄⟩ = ⟨𝑃, 𝑄⟩)
4443breq2d 5086 . . . . . . . 8 (𝑝 = 𝑃 → (𝑅 Btwn ⟨𝑝, 𝑄⟩ ↔ 𝑅 Btwn ⟨𝑃, 𝑄⟩))
4540, 42, 443orbi123d 1434 . . . . . . 7 (𝑝 = 𝑃 → ((𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩) ↔ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩)))
4639, 45anbi12d 631 . . . . . 6 (𝑝 = 𝑃 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩)) ↔ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
4746rexbidv 3226 . . . . 5 (𝑝 = 𝑃 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩)) ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
4827, 37, 47eloprabg 7384 . . . 4 ((𝑄𝑉𝑅𝑊𝑃 ∈ V) → (⟨⟨𝑄, 𝑅⟩, 𝑃⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))} ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
4917, 48bitrd 278 . . 3 ((𝑄𝑉𝑅𝑊𝑃 ∈ V) → (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
50493expia 1120 . 2 ((𝑄𝑉𝑅𝑊) → (𝑃 ∈ V → (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩)))))
513, 8, 50pm5.21ndd 381 1 ((𝑄𝑉𝑅𝑊) → (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3o 1085  w3a 1086   = wceq 1539  wcel 2106  wrex 3065  Vcvv 3432  cop 4567   class class class wbr 5074  ccnv 5588  cfv 6433  {coprab 7276  cn 11973  𝔼cee 27256   Btwn cbtwn 27257   Colinear ccolin 34339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-cnv 5597  df-oprab 7279  df-colinear 34341
This theorem is referenced by:  brcolinear  34361
  Copyright terms: Public domain W3C validator