ellines

Description: Membership in the set of all lines. (Contributed by Scott Fenton, 28-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	ellines	$⊢ A \in LinesEE \leftrightarrow \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land A = p Line q)$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in LinesEE \to A \in V$
2		ovex	$⊢ p Line q \in V$
3		eleq1	$⊢ A = p Line q \to (A \in V \leftrightarrow p Line q \in V)$
4	2 3	mpbiri	$⊢ A = p Line q \to A \in V$
5	4	adantl	$⊢ (p \neq q \land A = p Line q) \to A \in V$
6	5	rexlimivw	$⊢ \exists q \in 𝔼 (n) (p \neq q \land A = p Line q) \to A \in V$
7	6	a1i	$⊢ (n \in ℕ \land p \in 𝔼 (n)) \to (\exists q \in 𝔼 (n) (p \neq q \land A = p Line q) \to A \in V)$
8	7	rexlimivv	$⊢ \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land A = p Line q) \to A \in V$
9		eleq1	$⊢ x = A \to (x \in LinesEE \leftrightarrow A \in LinesEE)$
10		eqeq1	$⊢ x = A \to (x = p Line q \leftrightarrow A = p Line q)$
11	10	anbi2d	$⊢ x = A \to ((p \neq q \land x = p Line q) \leftrightarrow (p \neq q \land A = p Line q))$
12	11	rexbidv	$⊢ x = A \to (\exists q \in 𝔼 (n) (p \neq q \land x = p Line q) \leftrightarrow \exists q \in 𝔼 (n) (p \neq q \land A = p Line q))$
13	12	2rexbidv	$⊢ x = A \to (\exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land x = p Line q) \leftrightarrow \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land A = p Line q))$
14		df-lines2	$⊢ LinesEE = ran Line$
15		df-line2	$⊢ Line = \{⟨⟨p, q⟩, x⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})\}$
16	15	rneqi	$⊢ ran Line = ran \{⟨⟨p, q⟩, x⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})\}$
17		rnoprab	$⊢ ran \{⟨⟨p, q⟩, x⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})\} = \{x \| \exists p \exists q \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})\}$
18	14 16 17	3eqtri	$⊢ LinesEE = \{x \| \exists p \exists q \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})\}$
19	18	eleq2i	$⊢ x \in LinesEE \leftrightarrow x \in \{x \| \exists p \exists q \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})\}$
20		abid	$⊢ x \in \{x \| \exists p \exists q \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})\} \leftrightarrow \exists p \exists q \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})$
21		df-rex	$⊢ \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1}) \leftrightarrow \exists n (n \in ℕ \land ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1}))$
22	21	2exbii	$⊢ \exists p \exists q \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1}) \leftrightarrow \exists p \exists q \exists n (n \in ℕ \land ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1}))$
23		exrot3	$⊢ \exists n \exists p \exists q (q \in 𝔼 (n) \land ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q))) \leftrightarrow \exists p \exists q \exists n (q \in 𝔼 (n) \land ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q)))$
24		r2ex	$⊢ \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land x = p Line q) \leftrightarrow \exists n \exists p ((n \in ℕ \land p \in 𝔼 (n)) \land \exists q \in 𝔼 (n) (p \neq q \land x = p Line q))$
25		r19.42v	$⊢ \exists q \in 𝔼 (n) ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q)) \leftrightarrow ((n \in ℕ \land p \in 𝔼 (n)) \land \exists q \in 𝔼 (n) (p \neq q \land x = p Line q))$
26		df-rex	$⊢ \exists q \in 𝔼 (n) ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q)) \leftrightarrow \exists q (q \in 𝔼 (n) \land ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q)))$
27	25 26	bitr3i	$⊢ ((n \in ℕ \land p \in 𝔼 (n)) \land \exists q \in 𝔼 (n) (p \neq q \land x = p Line q)) \leftrightarrow \exists q (q \in 𝔼 (n) \land ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q)))$
28	27	2exbii	$⊢ \exists n \exists p ((n \in ℕ \land p \in 𝔼 (n)) \land \exists q \in 𝔼 (n) (p \neq q \land x = p Line q)) \leftrightarrow \exists n \exists p \exists q (q \in 𝔼 (n) \land ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q)))$
29	24 28	bitri	$⊢ \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land x = p Line q) \leftrightarrow \exists n \exists p \exists q (q \in 𝔼 (n) \land ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q)))$
30		anass	$⊢ ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land (p \neq q \land x = p Line q)) \leftrightarrow (q \in 𝔼 (n) \land ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q)))$
31		anass	$⊢ (((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land p \neq q) \land x = p Line q) \leftrightarrow ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land (p \neq q \land x = p Line q))$
32		simplrl	$⊢ ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land p \neq q) \to n \in ℕ$
33		simplrr	$⊢ ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land p \neq q) \to p \in 𝔼 (n)$
34		simpll	$⊢ ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land p \neq q) \to q \in 𝔼 (n)$
35		simpr	$⊢ ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land p \neq q) \to p \neq q$
36	33 34 35	3jca	$⊢ ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land p \neq q) \to (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)$
37	32 36	jca	$⊢ ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land p \neq q) \to (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q))$
38		simpr2	$⊢ (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \to q \in 𝔼 (n)$
39		simpl	$⊢ (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \to n \in ℕ$
40		simpr1	$⊢ (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \to p \in 𝔼 (n)$
41	38 39 40	jca32	$⊢ (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \to (q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n)))$
42		simpr3	$⊢ (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \to p \neq q$
43	41 42	jca	$⊢ (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \to ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land p \neq q)$
44	37 43	impbii	$⊢ ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land p \neq q) \leftrightarrow (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q))$
45	44	anbi1i	$⊢ (((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land p \neq q) \land x = p Line q) \leftrightarrow ((n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \land x = p Line q)$
46	31 45	bitr3i	$⊢ ((q \in 𝔼 (n) \land (n \in ℕ \land p \in 𝔼 (n))) \land (p \neq q \land x = p Line q)) \leftrightarrow ((n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \land x = p Line q)$
47	30 46	bitr3i	$⊢ (q \in 𝔼 (n) \land ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q))) \leftrightarrow ((n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \land x = p Line q)$
48		fvline	$⊢ (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \to p Line q = \{x \| x Colinear ⟨p, q⟩\}$
49		opex	$⊢ ⟨p, q⟩ \in V$
50		dfec2	$⊢ ⟨p, q⟩ \in V \to [⟨p, q⟩] {Colinear}^{-1} = \{x \| ⟨p, q⟩ {Colinear}^{-1} x\}$
51	49 50	ax-mp	$⊢ [⟨p, q⟩] {Colinear}^{-1} = \{x \| ⟨p, q⟩ {Colinear}^{-1} x\}$
52		vex	$⊢ x \in V$
53	49 52	brcnv	$⊢ ⟨p, q⟩ {Colinear}^{-1} x \leftrightarrow x Colinear ⟨p, q⟩$
54	53	abbii	$⊢ \{x \| ⟨p, q⟩ {Colinear}^{-1} x\} = \{x \| x Colinear ⟨p, q⟩\}$
55	51 54	eqtri	$⊢ [⟨p, q⟩] {Colinear}^{-1} = \{x \| x Colinear ⟨p, q⟩\}$
56	48 55	eqtr4di	$⊢ (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \to p Line q = [⟨p, q⟩] {Colinear}^{-1}$
57	56	eqeq2d	$⊢ (n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \to (x = p Line q \leftrightarrow x = [⟨p, q⟩] {Colinear}^{-1})$
58	57	pm5.32i	$⊢ ((n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \land x = p Line q) \leftrightarrow ((n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \land x = [⟨p, q⟩] {Colinear}^{-1})$
59		anass	$⊢ ((n \in ℕ \land (p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q)) \land x = [⟨p, q⟩] {Colinear}^{-1}) \leftrightarrow (n \in ℕ \land ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1}))$
60	47 58 59	3bitrri	$⊢ (n \in ℕ \land ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})) \leftrightarrow (q \in 𝔼 (n) \land ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q)))$
61	60	3exbii	$⊢ \exists p \exists q \exists n (n \in ℕ \land ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})) \leftrightarrow \exists p \exists q \exists n (q \in 𝔼 (n) \land ((n \in ℕ \land p \in 𝔼 (n)) \land (p \neq q \land x = p Line q)))$
62	23 29 61	3bitr4ri	$⊢ \exists p \exists q \exists n (n \in ℕ \land ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})) \leftrightarrow \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land x = p Line q)$
63	22 62	bitri	$⊢ \exists p \exists q \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1}) \leftrightarrow \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land x = p Line q)$
64	20 63	bitri	$⊢ x \in \{x \| \exists p \exists q \exists n \in ℕ ((p \in 𝔼 (n) \land q \in 𝔼 (n) \land p \neq q) \land x = [⟨p, q⟩] {Colinear}^{-1})\} \leftrightarrow \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land x = p Line q)$
65	19 64	bitri	$⊢ x \in LinesEE \leftrightarrow \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land x = p Line q)$
66	9 13 65	vtoclbg	$⊢ A \in V \to (A \in LinesEE \leftrightarrow \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land A = p Line q))$
67	1 8 66	pm5.21nii	$⊢ A \in LinesEE \leftrightarrow \exists n \in ℕ \exists p \in 𝔼 (n) \exists q \in 𝔼 (n) (p \neq q \land A = p Line q)$

Metamath Proof Explorer

Theorem ellines

Proof