Metamath Proof Explorer

Theorem colineardim1

Description: If A is colinear with B and C , then A is in the same space as B . (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion colineardim1 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 df-colinear ⊢ Colinear = ◡ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) }
2 1 breqi ⊢ ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐴 ◡ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } ⟨ 𝐵 , 𝐶 ⟩ )
3 simpr1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → 𝐴 ∈ 𝑉 )
4 opex ⊢ ⟨ 𝐵 , 𝐶 ⟩ ∈ V
5 brcnvg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ V ) → ( 𝐴 ◡ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } 𝐴 ) )
6 3 4 5 sylancl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( 𝐴 ◡ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } 𝐴 ) )
7 df-br ⊢ ( ⟨ 𝐵 , 𝐶 ⟩ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } 𝐴 ↔ ⟨ ⟨ 𝐵 , 𝐶 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } )
8 eleq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) )
9 8 3anbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
10 opeq1 ⊢ ( 𝑏 = 𝐵 → ⟨ 𝑏 , 𝑐 ⟩ = ⟨ 𝐵 , 𝑐 ⟩ )
11 10 breq2d ⊢ ( 𝑏 = 𝐵 → ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ↔ 𝑎 Btwn ⟨ 𝐵 , 𝑐 ⟩ ) )
12 breq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ↔ 𝐵 Btwn ⟨ 𝑐 , 𝑎 ⟩ ) )
13 opeq2 ⊢ ( 𝑏 = 𝐵 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑎 , 𝐵 ⟩ )
14 13 breq2d ⊢ ( 𝑏 = 𝐵 → ( 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑐 Btwn ⟨ 𝑎 , 𝐵 ⟩ ) )
15 11 12 14 3orbi123d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( 𝑎 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∨ 𝐵 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝐵 ⟩ ) ) )
16 9 15 anbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) ↔ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∨ 𝐵 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝐵 ⟩ ) ) ) )
17 16 rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝐵 , 𝑐 ⟩ ∨ 𝐵 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝐵 ⟩ ) ) ) )
18 eleq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) )
19 18 3anbi3d ⊢ ( 𝑐 = 𝐶 → ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
20 opeq2 ⊢ ( 𝑐 = 𝐶 → ⟨ 𝐵 , 𝑐 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
21 20 breq2d ⊢ ( 𝑐 = 𝐶 → ( 𝑎 Btwn ⟨ 𝐵 , 𝑐 ⟩ ↔ 𝑎 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
22 opeq1 ⊢ ( 𝑐 = 𝐶 → ⟨ 𝑐 , 𝑎 ⟩ = ⟨ 𝐶 , 𝑎 ⟩ )
23 22 breq2d ⊢ ( 𝑐 = 𝐶 → ( 𝐵 Btwn ⟨ 𝑐 , 𝑎 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝑎 ⟩ ) )
24 breq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 Btwn ⟨ 𝑎 , 𝐵 ⟩ ↔ 𝐶 Btwn ⟨ 𝑎 , 𝐵 ⟩ ) )
25 21 23 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 3anbi1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
30 breq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 Btwn ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ) )
31 opeq2 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝐶 , 𝑎 ⟩ = ⟨ 𝐶 , 𝐴 ⟩ )
32 31 breq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐵 Btwn ⟨ 𝐶 , 𝑎 ⟩ ↔ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ) )
33 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝐵 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
34 33 breq2d ⊢ ( 𝑎 = 𝐴 → ( 𝐶 Btwn ⟨ 𝑎 , 𝐵 ⟩ ↔ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) )
35 30 32 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 17 27 37 eloprabg ⊢ ( ( 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( ⟨ ⟨ 𝐵 , 𝐶 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
39 38 3comr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) → ( ⟨ ⟨ 𝐵 , 𝐶 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
40 39 adantl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( ⟨ ⟨ 𝐵 , 𝐶 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) ) )
41 simpl ⊢ ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) )
42 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
43 42 anim2i ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
44 3simpa ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) → ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) )
45 44 anim2i ⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ) → ( 𝑛 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ) )
46 axdimuniq ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑛 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ) → 𝑁 = 𝑛 )
47 46 adantrrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → 𝑁 = 𝑛 )
48 simprrl ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) )
49 fveq2 ⊢ ( 𝑁 = 𝑛 → ( 𝔼 ‘ 𝑁 ) = ( 𝔼 ‘ 𝑛 ) )
50 49 eleq2d ⊢ ( 𝑁 = 𝑛 → ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) )
51 48 50 syl5ibrcom ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → ( 𝑁 = 𝑛 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
52 47 51 mpd ⊢ ( ( ( 𝑁 ∈ ℕ ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
53 43 45 52 syl2an ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) ∧ ( 𝑛 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
54 53 exp32 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( 𝑛 ∈ ℕ → ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
55 41 54 syl7 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( 𝑛 ∈ ℕ → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) ) )
56 55 rexlimdv ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐶 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝐴 Btwn ⟨ 𝐵 , 𝐶 ⟩ ∨ 𝐵 Btwn ⟨ 𝐶 , 𝐴 ⟩ ∨ 𝐶 Btwn ⟨ 𝐴 , 𝐵 ⟩ ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
57 40 56 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( ⟨ ⟨ 𝐵 , 𝐶 ⟩ , 𝐴 ⟩ ∈ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
58 7 57 biimtrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( ⟨ 𝐵 , 𝐶 ⟩ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } 𝐴 → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
59 6 58 sylbid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( 𝐴 ◡ { ⟨ ⟨ 𝑏 , 𝑐 ⟩ , 𝑎 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑐 ∈ ( 𝔼 ‘ 𝑛 ) ) ∧ ( 𝑎 Btwn ⟨ 𝑏 , 𝑐 ⟩ ∨ 𝑏 Btwn ⟨ 𝑐 , 𝑎 ⟩ ∨ 𝑐 Btwn ⟨ 𝑎 , 𝑏 ⟩ ) ) } ⟨ 𝐵 , 𝐶 ⟩ → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
60 2 59 biimtrid ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐶 ∈ 𝑊 ) ) → ( 𝐴 Colinear ⟨ 𝐵 , 𝐶 ⟩ → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )