Theorem linedegen

Description: When Line is applied with the same argument, the result is the empty set. (Contributed by Scott Fenton, 29-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	linedegen	⊢ ( 𝐴 Line 𝐴 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-ov	⊢ ( 𝐴 Line 𝐴 ) = ( Line ‘ ⟨ 𝐴 , 𝐴 ⟩ )
2		neirr	⊢ ¬ 𝐴 ≠ 𝐴
3		simp3	⊢ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) → 𝐴 ≠ 𝐴 )
4	2 3	mto	⊢ ¬ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 )
5	4	intnanr	⊢ ¬ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear )
6	5	a1i	⊢ ( 𝑛 ∈ ℕ → ¬ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear ) )
7	6	nrex	⊢ ¬ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear )
8	7	nex	⊢ ¬ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear )
9		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) )
10		neeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≠ 𝑦 ↔ 𝐴 ≠ 𝑦 ) )
11	9 10	3anbi13d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑦 ) ) )
12		opeq1	⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
13	12	eceq1d	⊢ ( 𝑥 = 𝐴 → [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝑦 ⟩ ] ◡ Colinear )
14	13	eqeq2d	⊢ ( 𝑥 = 𝐴 → ( 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ↔ 𝑙 = [ ⟨ 𝐴 , 𝑦 ⟩ ] ◡ Colinear ) )
15	11 14	anbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) ↔ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝑦 ⟩ ] ◡ Colinear ) ) )
16	15	rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝑦 ⟩ ] ◡ Colinear ) ) )
17	16	exbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝑦 ⟩ ] ◡ Colinear ) ) )
18		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ↔ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ) )
19		neeq2	⊢ ( 𝑦 = 𝐴 → ( 𝐴 ≠ 𝑦 ↔ 𝐴 ≠ 𝐴 ) )
20	18 19	3anbi23d	⊢ ( 𝑦 = 𝐴 → ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑦 ) ↔ ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) ) )
21		opeq2	⊢ ( 𝑦 = 𝐴 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐴 ⟩ )
22	21	eceq1d	⊢ ( 𝑦 = 𝐴 → [ ⟨ 𝐴 , 𝑦 ⟩ ] ◡ Colinear = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear )
23	22	eqeq2d	⊢ ( 𝑦 = 𝐴 → ( 𝑙 = [ ⟨ 𝐴 , 𝑦 ⟩ ] ◡ Colinear ↔ 𝑙 = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear ) )
24	20 23	anbi12d	⊢ ( 𝑦 = 𝐴 → ( ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝑦 ⟩ ] ◡ Colinear ) ↔ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear ) ) )
25	24	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝑦 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear ) ) )
26	25	exbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝑦 ⟩ ] ◡ Colinear ) ↔ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear ) ) )
27	17 26	opelopabg	⊢ ( ( 𝐴 ∈ V ∧ 𝐴 ∈ V ) → ( ⟨ 𝐴 , 𝐴 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) } ↔ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear ) ) )
28	27	anidms	⊢ ( 𝐴 ∈ V → ( ⟨ 𝐴 , 𝐴 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) } ↔ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝐴 ≠ 𝐴 ) ∧ 𝑙 = [ ⟨ 𝐴 , 𝐴 ⟩ ] ◡ Colinear ) ) )
29	8 28	mtbiri	⊢ ( 𝐴 ∈ V → ¬ ⟨ 𝐴 , 𝐴 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) } )
30		elopaelxp	⊢ ( ⟨ 𝐴 , 𝐴 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) } → ⟨ 𝐴 , 𝐴 ⟩ ∈ ( V × V ) )
31		opelxp1	⊢ ( ⟨ 𝐴 , 𝐴 ⟩ ∈ ( V × V ) → 𝐴 ∈ V )
32	30 31	syl	⊢ ( ⟨ 𝐴 , 𝐴 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) } → 𝐴 ∈ V )
33	32	con3i	⊢ ( ¬ 𝐴 ∈ V → ¬ ⟨ 𝐴 , 𝐴 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) } )
34	29 33	pm2.61i	⊢ ¬ ⟨ 𝐴 , 𝐴 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) }
35		df-line2	⊢ Line = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) }
36	35	dmeqi	⊢ dom Line = dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) }
37		dmoprab	⊢ dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑙 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) }
38	36 37	eqtri	⊢ dom Line = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) }
39	38	eleq2i	⊢ ( ⟨ 𝐴 , 𝐴 ⟩ ∈ dom Line ↔ ⟨ 𝐴 , 𝐴 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑙 ∃ 𝑛 ∈ ℕ ( ( 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑦 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑥 ≠ 𝑦 ) ∧ 𝑙 = [ ⟨ 𝑥 , 𝑦 ⟩ ] ◡ Colinear ) } )
40	34 39	mtbir	⊢ ¬ ⟨ 𝐴 , 𝐴 ⟩ ∈ dom Line
41		ndmfv	⊢ ( ¬ ⟨ 𝐴 , 𝐴 ⟩ ∈ dom Line → ( Line ‘ ⟨ 𝐴 , 𝐴 ⟩ ) = ∅ )
42	40 41	ax-mp	⊢ ( Line ‘ ⟨ 𝐴 , 𝐴 ⟩ ) = ∅
43	1 42	eqtri	⊢ ( 𝐴 Line 𝐴 ) = ∅