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	$⊢ A Line A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		df-ov	$⊢ A Line A = Line (⟨A, A⟩)$
2		neirr	$⊢ \neg A \neq A$
3		simp3	$⊢ (A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A) \to A \neq A$
4	2 3	mto	$⊢ \neg (A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A)$
5	4	intnanr	$⊢ \neg ((A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A) \land l = [⟨A, A⟩] {Colinear}^{-1})$
6	5	a1i	$⊢ n \in ℕ \to \neg ((A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A) \land l = [⟨A, A⟩] {Colinear}^{-1})$
7	6	nrex	$⊢ \neg \exists n \in ℕ ((A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A) \land l = [⟨A, A⟩] {Colinear}^{-1})$
8	7	nex	$⊢ \neg \exists l \exists n \in ℕ ((A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A) \land l = [⟨A, A⟩] {Colinear}^{-1})$
9		eleq1	$⊢ x = A \to (x \in 𝔼 (n) \leftrightarrow A \in 𝔼 (n))$
10		neeq1	$⊢ x = A \to (x \neq y \leftrightarrow A \neq y)$
11	9 10	3anbi13d	$⊢ x = A \to ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \leftrightarrow (A \in 𝔼 (n) \land y \in 𝔼 (n) \land A \neq y))$
12		opeq1	$⊢ x = A \to ⟨x, y⟩ = ⟨A, y⟩$
13	12	eceq1d	$⊢ x = A \to [⟨x, y⟩] {Colinear}^{-1} = [⟨A, y⟩] {Colinear}^{-1}$
14	13	eqeq2d	$⊢ x = A \to (l = [⟨x, y⟩] {Colinear}^{-1} \leftrightarrow l = [⟨A, y⟩] {Colinear}^{-1})$
15	11 14	anbi12d	$⊢ x = A \to (((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1}) \leftrightarrow ((A \in 𝔼 (n) \land y \in 𝔼 (n) \land A \neq y) \land l = [⟨A, y⟩] {Colinear}^{-1}))$
16	15	rexbidv	$⊢ x = A \to (\exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1}) \leftrightarrow \exists n \in ℕ ((A \in 𝔼 (n) \land y \in 𝔼 (n) \land A \neq y) \land l = [⟨A, y⟩] {Colinear}^{-1}))$
17	16	exbidv	$⊢ x = A \to (\exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1}) \leftrightarrow \exists l \exists n \in ℕ ((A \in 𝔼 (n) \land y \in 𝔼 (n) \land A \neq y) \land l = [⟨A, y⟩] {Colinear}^{-1}))$
18		eleq1	$⊢ y = A \to (y \in 𝔼 (n) \leftrightarrow A \in 𝔼 (n))$
19		neeq2	$⊢ y = A \to (A \neq y \leftrightarrow A \neq A)$
20	18 19	3anbi23d	$⊢ y = A \to ((A \in 𝔼 (n) \land y \in 𝔼 (n) \land A \neq y) \leftrightarrow (A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A))$
21		opeq2	$⊢ y = A \to ⟨A, y⟩ = ⟨A, A⟩$
22	21	eceq1d	$⊢ y = A \to [⟨A, y⟩] {Colinear}^{-1} = [⟨A, A⟩] {Colinear}^{-1}$
23	22	eqeq2d	$⊢ y = A \to (l = [⟨A, y⟩] {Colinear}^{-1} \leftrightarrow l = [⟨A, A⟩] {Colinear}^{-1})$
24	20 23	anbi12d	$⊢ y = A \to (((A \in 𝔼 (n) \land y \in 𝔼 (n) \land A \neq y) \land l = [⟨A, y⟩] {Colinear}^{-1}) \leftrightarrow ((A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A) \land l = [⟨A, A⟩] {Colinear}^{-1}))$
25	24	rexbidv	$⊢ y = A \to (\exists n \in ℕ ((A \in 𝔼 (n) \land y \in 𝔼 (n) \land A \neq y) \land l = [⟨A, y⟩] {Colinear}^{-1}) \leftrightarrow \exists n \in ℕ ((A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A) \land l = [⟨A, A⟩] {Colinear}^{-1}))$
26	25	exbidv	$⊢ y = A \to (\exists l \exists n \in ℕ ((A \in 𝔼 (n) \land y \in 𝔼 (n) \land A \neq y) \land l = [⟨A, y⟩] {Colinear}^{-1}) \leftrightarrow \exists l \exists n \in ℕ ((A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A) \land l = [⟨A, A⟩] {Colinear}^{-1}))$
27	17 26	opelopabg	$⊢ (A \in V \land A \in V) \to (⟨A, A⟩ \in \{⟨x, y⟩ \| \exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\} \leftrightarrow \exists l \exists n \in ℕ ((A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A) \land l = [⟨A, A⟩] {Colinear}^{-1}))$
28	27	anidms	$⊢ A \in V \to (⟨A, A⟩ \in \{⟨x, y⟩ \| \exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\} \leftrightarrow \exists l \exists n \in ℕ ((A \in 𝔼 (n) \land A \in 𝔼 (n) \land A \neq A) \land l = [⟨A, A⟩] {Colinear}^{-1}))$
29	8 28	mtbiri	$⊢ A \in V \to \neg ⟨A, A⟩ \in \{⟨x, y⟩ \| \exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\}$
30		elopaelxp	$⊢ ⟨A, A⟩ \in \{⟨x, y⟩ \| \exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\} \to ⟨A, A⟩ \in (V \times V)$
31		opelxp1	$⊢ ⟨A, A⟩ \in (V \times V) \to A \in V$
32	30 31	syl	$⊢ ⟨A, A⟩ \in \{⟨x, y⟩ \| \exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\} \to A \in V$
33	32	con3i	$⊢ \neg A \in V \to \neg ⟨A, A⟩ \in \{⟨x, y⟩ \| \exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\}$
34	29 33	pm2.61i	$⊢ \neg ⟨A, A⟩ \in \{⟨x, y⟩ \| \exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\}$
35		df-line2	$⊢ Line = \{⟨⟨x, y⟩, l⟩ \| \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\}$
36	35	dmeqi	$⊢ dom Line = dom \{⟨⟨x, y⟩, l⟩ \| \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\}$
37		dmoprab	$⊢ dom \{⟨⟨x, y⟩, l⟩ \| \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\} = \{⟨x, y⟩ \| \exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\}$
38	36 37	eqtri	$⊢ dom Line = \{⟨x, y⟩ \| \exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\}$
39	38	eleq2i	$⊢ ⟨A, A⟩ \in dom Line \leftrightarrow ⟨A, A⟩ \in \{⟨x, y⟩ \| \exists l \exists n \in ℕ ((x \in 𝔼 (n) \land y \in 𝔼 (n) \land x \neq y) \land l = [⟨x, y⟩] {Colinear}^{-1})\}$
40	34 39	mtbir	$⊢ \neg ⟨A, A⟩ \in dom Line$
41		ndmfv	$⊢ \neg ⟨A, A⟩ \in dom Line \to Line (⟨A, A⟩) = \emptyset$
42	40 41	ax-mp	$⊢ Line (⟨A, A⟩) = \emptyset$
43	1 42	eqtri	$⊢ A Line A = \emptyset$

Metamath Proof Explorer

Theorem linedegen

Proof