Metamath Proof Explorer

Theorem brcolinear2

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

Ref Expression
Assertion brcolinear2 ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑃 Colinear ⟨ 𝑄 , 𝑅 ⟩ ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) ) )

Proof

Step Hyp Ref Expression
1 colinrel ⊢ Rel Colinear
2 1 brrelex1i ⊢ ( 𝑃 Colinear ⟨ 𝑄 , 𝑅 ⟩ → 𝑃 ∈ V )
3 2 a1i ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑃 Colinear ⟨ 𝑄 , 𝑅 ⟩ → 𝑃 ∈ V ) )
4 elex ⊢ ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) → 𝑃 ∈ V )
5 4 3ad2ant1 ⊢ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) → 𝑃 ∈ V )
6 5 adantr ⊢ ( ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) → 𝑃 ∈ V )
7 6 rexlimivw ⊢ ( ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) → 𝑃 ∈ V )
8 7 a1i ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) → 𝑃 ∈ V ) )
9 df-br ⊢ ( 𝑃 Colinear ⟨ 𝑄 , 𝑅 ⟩ ↔ ⟨ 𝑃 , ⟨ 𝑄 , 𝑅 ⟩ ⟩ ∈ Colinear )
10 df-colinear ⊢ Colinear = ◡ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) }
11 10 eleq2i ⊢ ( ⟨ 𝑃 , ⟨ 𝑄 , 𝑅 ⟩ ⟩ ∈ Colinear ↔ ⟨ 𝑃 , ⟨ 𝑄 , 𝑅 ⟩ ⟩ ∈ ◡ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } )
12 9 11 bitri ⊢ ( 𝑃 Colinear ⟨ 𝑄 , 𝑅 ⟩ ↔ ⟨ 𝑃 , ⟨ 𝑄 , 𝑅 ⟩ ⟩ ∈ ◡ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } )
13 opex ⊢ ⟨ 𝑄 , 𝑅 ⟩ ∈ V
14 opelcnvg ⊢ ( ( 𝑃 ∈ V ∧ ⟨ 𝑄 , 𝑅 ⟩ ∈ V ) → ( ⟨ 𝑃 , ⟨ 𝑄 , 𝑅 ⟩ ⟩ ∈ ◡ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } ↔ ⟨ ⟨ 𝑄 , 𝑅 ⟩ , 𝑃 ⟩ ∈ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } ) )
15 13 14 mpan2 ⊢ ( 𝑃 ∈ V → ( ⟨ 𝑃 , ⟨ 𝑄 , 𝑅 ⟩ ⟩ ∈ ◡ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } ↔ ⟨ ⟨ 𝑄 , 𝑅 ⟩ , 𝑃 ⟩ ∈ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } ) )
16 15 3ad2ant3 ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑃 ∈ V ) → ( ⟨ 𝑃 , ⟨ 𝑄 , 𝑅 ⟩ ⟩ ∈ ◡ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } ↔ ⟨ ⟨ 𝑄 , 𝑅 ⟩ , 𝑃 ⟩ ∈ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } ) )
17 12 16 bitrid ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑃 ∈ V ) → ( 𝑃 Colinear ⟨ 𝑄 , 𝑅 ⟩ ↔ ⟨ ⟨ 𝑄 , 𝑅 ⟩ , 𝑃 ⟩ ∈ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } ) )
18 eleq1 ⊢ ( 𝑞 = 𝑄 → ( 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ) )
19 18 3anbi2d ⊢ ( 𝑞 = 𝑄 → ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
20 opeq1 ⊢ ( 𝑞 = 𝑄 → ⟨ 𝑞 , 𝑟 ⟩ = ⟨ 𝑄 , 𝑟 ⟩ )
21 20 breq2d ⊢ ( 𝑞 = 𝑄 → ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ↔ 𝑝 Btwn ⟨ 𝑄 , 𝑟 ⟩ ) )
22 breq1 ⊢ ( 𝑞 = 𝑄 → ( 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ↔ 𝑄 Btwn ⟨ 𝑟 , 𝑝 ⟩ ) )
23 opeq2 ⊢ ( 𝑞 = 𝑄 → ⟨ 𝑝 , 𝑞 ⟩ = ⟨ 𝑝 , 𝑄 ⟩ )
24 23 breq2d ⊢ ( 𝑞 = 𝑄 → ( 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ↔ 𝑟 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) )
25 21 22 24 3orbi123d ⊢ ( 𝑞 = 𝑄 → ( ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ↔ ( 𝑝 Btwn ⟨ 𝑄 , 𝑟 ⟩ ∨ 𝑄 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ) )
26 19 25 anbi12d ⊢ ( 𝑞 = 𝑄 → ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) ↔ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑄 , 𝑟 ⟩ ∨ 𝑄 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ) ) )
27 26 rexbidv ⊢ ( 𝑞 = 𝑄 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑄 , 𝑟 ⟩ ∨ 𝑄 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ) ) )
28 eleq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) )
29 28 3anbi3d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
30 opeq2 ⊢ ( 𝑟 = 𝑅 → ⟨ 𝑄 , 𝑟 ⟩ = ⟨ 𝑄 , 𝑅 ⟩ )
31 30 breq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑝 Btwn ⟨ 𝑄 , 𝑟 ⟩ ↔ 𝑝 Btwn ⟨ 𝑄 , 𝑅 ⟩ ) )
32 opeq1 ⊢ ( 𝑟 = 𝑅 → ⟨ 𝑟 , 𝑝 ⟩ = ⟨ 𝑅 , 𝑝 ⟩ )
33 32 breq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑄 Btwn ⟨ 𝑟 , 𝑝 ⟩ ↔ 𝑄 Btwn ⟨ 𝑅 , 𝑝 ⟩ ) )
34 breq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 Btwn ⟨ 𝑝 , 𝑄 ⟩ ↔ 𝑅 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) )
35 31 33 34 3orbi123d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑝 Btwn ⟨ 𝑄 , 𝑟 ⟩ ∨ 𝑄 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ↔ ( 𝑝 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑝 ⟩ ∨ 𝑅 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ) )
36 29 35 anbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑄 , 𝑟 ⟩ ∨ 𝑄 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ) ↔ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑝 ⟩ ∨ 𝑅 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ) ) )
37 36 rexbidv ⊢ ( 𝑟 = 𝑅 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑄 , 𝑟 ⟩ ∨ 𝑄 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑝 ⟩ ∨ 𝑅 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ) ) )
38 eleq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ) )
39 38 3anbi1d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
40 breq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 Btwn ⟨ 𝑄 , 𝑅 ⟩ ↔ 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ) )
41 opeq2 ⊢ ( 𝑝 = 𝑃 → ⟨ 𝑅 , 𝑝 ⟩ = ⟨ 𝑅 , 𝑃 ⟩ )
42 41 breq2d ⊢ ( 𝑝 = 𝑃 → ( 𝑄 Btwn ⟨ 𝑅 , 𝑝 ⟩ ↔ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ) )
43 opeq1 ⊢ ( 𝑝 = 𝑃 → ⟨ 𝑝 , 𝑄 ⟩ = ⟨ 𝑃 , 𝑄 ⟩ )
44 43 breq2d ⊢ ( 𝑝 = 𝑃 → ( 𝑅 Btwn ⟨ 𝑝 , 𝑄 ⟩ ↔ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) )
45 40 42 44 3orbi123d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑝 ⟩ ∨ 𝑅 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ↔ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) )
46 39 45 anbi12d ⊢ ( 𝑝 = 𝑃 → ( ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑝 ⟩ ∨ 𝑅 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ) ↔ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) ) )
47 46 rexbidv ⊢ ( 𝑝 = 𝑃 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑝 ⟩ ∨ 𝑅 Btwn ⟨ 𝑝 , 𝑄 ⟩ ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) ) )
48 27 37 47 eloprabg ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑃 ∈ V ) → ( ⟨ ⟨ 𝑄 , 𝑅 ⟩ , 𝑃 ⟩ ∈ { ⟨ ⟨ 𝑞 , 𝑟 ⟩ , 𝑝 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑞 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑟 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑝 Btwn ⟨ 𝑞 , 𝑟 ⟩ ∨ 𝑞 Btwn ⟨ 𝑟 , 𝑝 ⟩ ∨ 𝑟 Btwn ⟨ 𝑝 , 𝑞 ⟩ ) ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) ) )
49 17 48 bitrd ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ 𝑃 ∈ V ) → ( 𝑃 Colinear ⟨ 𝑄 , 𝑅 ⟩ ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) ) )
50 49 3expia ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑃 ∈ V → ( 𝑃 Colinear ⟨ 𝑄 , 𝑅 ⟩ ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) ) ) )
51 3 8 50 pm5.21ndd ⊢ ( ( 𝑄 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑃 Colinear ⟨ 𝑄 , 𝑅 ⟩ ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑃 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑄 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑅 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑃 Btwn ⟨ 𝑄 , 𝑅 ⟩ ∨ 𝑄 Btwn ⟨ 𝑅 , 𝑃 ⟩ ∨ 𝑅 Btwn ⟨ 𝑃 , 𝑄 ⟩ ) ) ) )