Theorem funline

Description: Show that the Line relationship is a function. (Contributed by Scott Fenton, 25-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	funline	⊢ Fun Line

Proof

Step	Hyp	Ref	Expression
1		reeanv	⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ∧ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) ↔ ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) )
2		eqtr3	⊢ ( ( 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) → 𝑙 = 𝑘 )
3	2	ad2ant2l	⊢ ( ( ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ∧ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) → 𝑙 = 𝑘 )
4	3	a1i	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( ( ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ∧ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) → 𝑙 = 𝑘 ) )
5	4	rexlimivv	⊢ ( ∃ 𝑛 ∈ ℕ ∃ 𝑚 ∈ ℕ ( ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ∧ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) → 𝑙 = 𝑘 )
6	1 5	sylbir	⊢ ( ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) → 𝑙 = 𝑘 )
7	6	gen2	⊢ ∀ 𝑙 ∀ 𝑘 ( ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) → 𝑙 = 𝑘 )
8		eqeq1	⊢ ( 𝑙 = 𝑘 → ( 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ↔ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) )
9	8	anbi2d	⊢ ( 𝑙 = 𝑘 → ( ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ↔ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) )
10	9	rexbidv	⊢ ( 𝑙 = 𝑘 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) )
11		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝔼 ‘ 𝑛 ) = ( 𝔼 ‘ 𝑚 ) )
12	11	eleq2d	⊢ ( 𝑛 = 𝑚 → ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ) )
13	11	eleq2d	⊢ ( 𝑛 = 𝑚 → ( 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ) )
14	12 13	3anbi12d	⊢ ( 𝑛 = 𝑚 → ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ↔ ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ) )
15	14	anbi1d	⊢ ( 𝑛 = 𝑚 → ( ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ↔ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) )
16	15	cbvrexvw	⊢ ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑚 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) )
17	10 16	bitrdi	⊢ ( 𝑙 = 𝑘 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑚 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) )
18	17	mo4	⊢ ( ∃* 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ↔ ∀ 𝑙 ∀ 𝑘 ( ( ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ∧ ∃ 𝑚 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑚 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑘 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) ) → 𝑙 = 𝑘 ) )
19	7 18	mpbir	⊢ ∃* 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear )
20	19	funoprab	⊢ Fun { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) }
21		df-line2	⊢ Line = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) }
22	21	funeqi	⊢ ( Fun Line ↔ Fun { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑏 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ≠ 𝑏 ) ∧ 𝑙 = [ ⟨ 𝑎 , 𝑏 ⟩ ] ◡ Colinear ) } )
23	20 22	mpbir	⊢ Fun Line