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 32471
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 32470 . . . 4 Rel Colinear
21brrelexi 5315 . . 3 (𝑃 Colinear ⟨𝑄, 𝑅⟩ → 𝑃 ∈ V)
32a1i 11 . 2 ((𝑄𝑉𝑅𝑊) → (𝑃 Colinear ⟨𝑄, 𝑅⟩ → 𝑃 ∈ V))
4 elex 3352 . . . . . 6 (𝑃 ∈ (𝔼‘𝑛) → 𝑃 ∈ V)
543ad2ant1 1128 . . . . 5 ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) → 𝑃 ∈ V)
65adantr 472 . . . 4 (((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 ∈ V)
76rexlimivw 3167 . . 3 (∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 ∈ V)
87a1i 11 . 2 ((𝑄𝑉𝑅𝑊) → (∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩)) → 𝑃 ∈ V))
9 df-br 4805 . . . . . 6 (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ Colinear )
10 df-colinear 32452 . . . . . . 7 Colinear = {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))}
1110eleq2i 2831 . . . . . 6 (⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ Colinear ↔ ⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))})
129, 11bitri 264 . . . . 5 (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))})
13 opex 5081 . . . . . . 7 𝑄, 𝑅⟩ ∈ V
14 opelcnvg 5457 . . . . . . 7 ((𝑃 ∈ V ∧ ⟨𝑄, 𝑅⟩ ∈ V) → (⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))} ↔ ⟨⟨𝑄, 𝑅⟩, 𝑃⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))}))
1513, 14mpan2 709 . . . . . 6 (𝑃 ∈ V → (⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))} ↔ ⟨⟨𝑄, 𝑅⟩, 𝑃⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))}))
16153ad2ant3 1130 . . . . 5 ((𝑄𝑉𝑅𝑊𝑃 ∈ V) → (⟨𝑃, ⟨𝑄, 𝑅⟩⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))} ↔ ⟨⟨𝑄, 𝑅⟩, 𝑃⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))}))
1712, 16syl5bb 272 . . . 4 ((𝑄𝑉𝑅𝑊𝑃 ∈ V) → (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ⟨⟨𝑄, 𝑅⟩, 𝑃⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))}))
18 eleq1 2827 . . . . . . . 8 (𝑞 = 𝑄 → (𝑞 ∈ (𝔼‘𝑛) ↔ 𝑄 ∈ (𝔼‘𝑛)))
19183anbi2d 1553 . . . . . . 7 (𝑞 = 𝑄 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ↔ (𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛))))
20 opeq1 4553 . . . . . . . . 9 (𝑞 = 𝑄 → ⟨𝑞, 𝑟⟩ = ⟨𝑄, 𝑟⟩)
2120breq2d 4816 . . . . . . . 8 (𝑞 = 𝑄 → (𝑝 Btwn ⟨𝑞, 𝑟⟩ ↔ 𝑝 Btwn ⟨𝑄, 𝑟⟩))
22 breq1 4807 . . . . . . . 8 (𝑞 = 𝑄 → (𝑞 Btwn ⟨𝑟, 𝑝⟩ ↔ 𝑄 Btwn ⟨𝑟, 𝑝⟩))
23 opeq2 4554 . . . . . . . . 9 (𝑞 = 𝑄 → ⟨𝑝, 𝑞⟩ = ⟨𝑝, 𝑄⟩)
2423breq2d 4816 . . . . . . . 8 (𝑞 = 𝑄 → (𝑟 Btwn ⟨𝑝, 𝑞⟩ ↔ 𝑟 Btwn ⟨𝑝, 𝑄⟩))
2521, 22, 243orbi123d 1547 . . . . . . 7 (𝑞 = 𝑄 → ((𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩) ↔ (𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩)))
2619, 25anbi12d 749 . . . . . 6 (𝑞 = 𝑄 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩)) ↔ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩))))
2726rexbidv 3190 . . . . 5 (𝑞 = 𝑄 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩)) ↔ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩))))
28 eleq1 2827 . . . . . . . 8 (𝑟 = 𝑅 → (𝑟 ∈ (𝔼‘𝑛) ↔ 𝑅 ∈ (𝔼‘𝑛)))
29283anbi3d 1554 . . . . . . 7 (𝑟 = 𝑅 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ↔ (𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛))))
30 opeq2 4554 . . . . . . . . 9 (𝑟 = 𝑅 → ⟨𝑄, 𝑟⟩ = ⟨𝑄, 𝑅⟩)
3130breq2d 4816 . . . . . . . 8 (𝑟 = 𝑅 → (𝑝 Btwn ⟨𝑄, 𝑟⟩ ↔ 𝑝 Btwn ⟨𝑄, 𝑅⟩))
32 opeq1 4553 . . . . . . . . 9 (𝑟 = 𝑅 → ⟨𝑟, 𝑝⟩ = ⟨𝑅, 𝑝⟩)
3332breq2d 4816 . . . . . . . 8 (𝑟 = 𝑅 → (𝑄 Btwn ⟨𝑟, 𝑝⟩ ↔ 𝑄 Btwn ⟨𝑅, 𝑝⟩))
34 breq1 4807 . . . . . . . 8 (𝑟 = 𝑅 → (𝑟 Btwn ⟨𝑝, 𝑄⟩ ↔ 𝑅 Btwn ⟨𝑝, 𝑄⟩))
3531, 33, 343orbi123d 1547 . . . . . . 7 (𝑟 = 𝑅 → ((𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩) ↔ (𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩)))
3629, 35anbi12d 749 . . . . . 6 (𝑟 = 𝑅 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩)) ↔ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩))))
3736rexbidv 3190 . . . . 5 (𝑟 = 𝑅 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑟⟩ ∨ 𝑄 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑄⟩)) ↔ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩))))
38 eleq1 2827 . . . . . . . 8 (𝑝 = 𝑃 → (𝑝 ∈ (𝔼‘𝑛) ↔ 𝑃 ∈ (𝔼‘𝑛)))
39383anbi1d 1552 . . . . . . 7 (𝑝 = 𝑃 → ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ↔ (𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛))))
40 breq1 4807 . . . . . . . 8 (𝑝 = 𝑃 → (𝑝 Btwn ⟨𝑄, 𝑅⟩ ↔ 𝑃 Btwn ⟨𝑄, 𝑅⟩))
41 opeq2 4554 . . . . . . . . 9 (𝑝 = 𝑃 → ⟨𝑅, 𝑝⟩ = ⟨𝑅, 𝑃⟩)
4241breq2d 4816 . . . . . . . 8 (𝑝 = 𝑃 → (𝑄 Btwn ⟨𝑅, 𝑝⟩ ↔ 𝑄 Btwn ⟨𝑅, 𝑃⟩))
43 opeq1 4553 . . . . . . . . 9 (𝑝 = 𝑃 → ⟨𝑝, 𝑄⟩ = ⟨𝑃, 𝑄⟩)
4443breq2d 4816 . . . . . . . 8 (𝑝 = 𝑃 → (𝑅 Btwn ⟨𝑝, 𝑄⟩ ↔ 𝑅 Btwn ⟨𝑃, 𝑄⟩))
4540, 42, 443orbi123d 1547 . . . . . . 7 (𝑝 = 𝑃 → ((𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩) ↔ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩)))
4639, 45anbi12d 749 . . . . . 6 (𝑝 = 𝑃 → (((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩)) ↔ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
4746rexbidv 3190 . . . . 5 (𝑝 = 𝑃 → (∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑝⟩ ∨ 𝑅 Btwn ⟨𝑝, 𝑄⟩)) ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
4827, 37, 47eloprabg 6913 . . . 4 ((𝑄𝑉𝑅𝑊𝑃 ∈ V) → (⟨⟨𝑄, 𝑅⟩, 𝑃⟩ ∈ {⟨⟨𝑞, 𝑟⟩, 𝑝⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑞 ∈ (𝔼‘𝑛) ∧ 𝑟 ∈ (𝔼‘𝑛)) ∧ (𝑝 Btwn ⟨𝑞, 𝑟⟩ ∨ 𝑞 Btwn ⟨𝑟, 𝑝⟩ ∨ 𝑟 Btwn ⟨𝑝, 𝑞⟩))} ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
4917, 48bitrd 268 . . 3 ((𝑄𝑉𝑅𝑊𝑃 ∈ V) → (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
50493expia 1115 . 2 ((𝑄𝑉𝑅𝑊) → (𝑃 ∈ V → (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩)))))
513, 8, 50pm5.21ndd 368 1 ((𝑄𝑉𝑅𝑊) → (𝑃 Colinear ⟨𝑄, 𝑅⟩ ↔ ∃𝑛 ∈ ℕ ((𝑃 ∈ (𝔼‘𝑛) ∧ 𝑄 ∈ (𝔼‘𝑛) ∧ 𝑅 ∈ (𝔼‘𝑛)) ∧ (𝑃 Btwn ⟨𝑄, 𝑅⟩ ∨ 𝑄 Btwn ⟨𝑅, 𝑃⟩ ∨ 𝑅 Btwn ⟨𝑃, 𝑄⟩))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3o 1071  w3a 1072   = wceq 1632  wcel 2139  wrex 3051  Vcvv 3340  cop 4327   class class class wbr 4804  ccnv 5265  cfv 6049  {coprab 6814  cn 11212  𝔼cee 25967   Btwn cbtwn 25968   Colinear ccolin 32450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-xp 5272  df-rel 5273  df-cnv 5274  df-oprab 6817  df-colinear 32452
This theorem is referenced by:  brcolinear  32472
  Copyright terms: Public domain W3C validator