Metamath Proof Explorer

Theorem fvline

Description: Calculate the value of the Line function. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fvline ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } )

Proof

Step Hyp Ref Expression
1 eqid ⊢ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear
2 fveq2 ⊢ ( 𝑛 = 𝑁 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑁 ) )
3 2 eleq2d ⊢ ( 𝑛 = 𝑁 → ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ) )
4 2 eleq2d ⊢ ( 𝑛 = 𝑁 → ( 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) )
5 3 4 3anbi12d ⊢ ( 𝑛 = 𝑁 → ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) )
6 5 anbi1d ⊢ ( 𝑛 = 𝑁 → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ↔ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ) )
7 6 rspcev ⊢ ( ( 𝑁 ∈ ℕ ∧ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) )
8 1 7 mpanr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) )
9 simpr1 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) )
10 simpr2 ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) )
11 colinearex ⊢ Colinear ∈ V
12 11 cnvex ⊢ ◡ Colinear ∈ V
13 ecexg ⊢ ( ◡ Colinear ∈ V → [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ∈ V )
14 12 13 ax-mp ⊢ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ∈ V
15 eleq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) )
16 neeq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ≠ 𝑏 ↔ 𝐴 ≠ 𝑏 ) )
17 15 16 3anbi13d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑏 ) ) )
18 opeq1 ⊢ ( 𝑎 = 𝐴 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝐴 , 𝑏 ⟩ )
19 18 eceq1d ⊢ ( 𝑎 = 𝐴 → [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝑏 ⟩ ] ◡ Colinear )
20 19 eqeq2d ⊢ ( 𝑎 = 𝐴 → ( 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ↔ 𝑙 = [ ⟨ 𝐴 , 𝑏 ⟩ ] ◡ Colinear ) )
21 17 20 anbi12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ↔ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝑏 ⟩ ] ◡ Colinear ) ) )
22 21 rexbidv ⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝑏 ⟩ ] ◡ Colinear ) ) )
23 eleq1 ⊢ ( 𝑏 = 𝐵 → ( 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ) )
24 neeq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 ≠ 𝑏 ↔ 𝐴 ≠ 𝐵 ) )
25 23 24 3anbi23d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑏 ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ) )
26 opeq2 ⊢ ( 𝑏 = 𝐵 → ⟨ 𝐴 , 𝑏 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
27 26 eceq1d ⊢ ( 𝑏 = 𝐵 → [ ⟨ 𝐴 , 𝑏 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear )
28 27 eqeq2d ⊢ ( 𝑏 = 𝐵 → ( 𝑙 = [ ⟨ 𝐴 , 𝑏 ⟩ ] ◡ Colinear ↔ 𝑙 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) )
29 25 28 anbi12d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝑏 ⟩ ] ◡ Colinear ) ↔ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ) )
30 29 rexbidv ⊢ ( 𝑏 = 𝐵 → ( ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝑏 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ) )
31 eqeq1 ⊢ ( 𝑙 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear → ( 𝑙 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ↔ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) )
32 31 anbi2d ⊢ ( 𝑙 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ↔ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ) )
33 32 rexbidv ⊢ ( 𝑙 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear → ( ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ) )
34 22 30 33 eloprabg ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ∈ V ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ) )
35 14 34 mp3an3 ⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ) )
36 9 10 35 syl2anc ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) } ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐵 ) ∧ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) ) )
37 8 36 mpbird ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ⟨ ⟨ 𝐴 , 𝐵 ⟩ , [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) } )
38 df-ov ⊢ ( 𝐴 Line 𝐵 ) = ( Line ‘ ⟨ 𝐴 , 𝐵 ⟩ )
39 df-br ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Line [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ⟩ ∈ Line )
40 df-line2 ⊢ Line = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) }
41 40 eleq2i ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ⟩ ∈ Line ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) } )
42 39 41 bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Line [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) } )
43 funline ⊢ Fun Line
44 funbrfv ⊢ ( Fun Line → ( ⟨ 𝐴 , 𝐵 ⟩ Line [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear → ( Line ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ) )
45 43 44 ax-mp ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Line [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear → ( Line ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear )
46 42 45 sylbir ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) } → ( Line ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear )
47 38 46 syl5eq ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) } → ( 𝐴 Line 𝐵 ) = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear )
48 37 47 syl ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) = [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear )
49 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
50 dfec2 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V → [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = { 𝑥 ∣ ⟨ 𝐴 , 𝐵 ⟩ ◡ Colinear 𝑥 } )
51 49 50 ax-mp ⊢ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = { 𝑥 ∣ ⟨ 𝐴 , 𝐵 ⟩ ◡ Colinear 𝑥 }
52 vex ⊢ 𝑥 ∈ V
53 49 52 brcnv ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ◡ Colinear 𝑥 ↔ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ )
54 53 abbii ⊢ { 𝑥 ∣ ⟨ 𝐴 , 𝐵 ⟩ ◡ Colinear 𝑥 } = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ }
55 51 54 eqtri ⊢ [ ⟨ 𝐴 , 𝐵 ⟩ ] ◡ Colinear = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ }
56 48 55 eqtrdi ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐴 ≠ 𝐵 ) ) → ( 𝐴 Line 𝐵 ) = { 𝑥 ∣ 𝑥 Colinear ⟨ 𝐴 , 𝐵 ⟩ } )