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	$⊢ \exists n \in ℕ \exists m \in ℕ (((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \land ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1})) \leftrightarrow (\exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \land \exists m \in ℕ ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1}))$
2		eqtr3	$⊢ (l = [⟨a, b⟩] {Colinear}^{-1} \land k = [⟨a, b⟩] {Colinear}^{-1}) \to l = k$
3	2	ad2ant2l	$⊢ (((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \land ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1})) \to l = k$
4	3	a1i	$⊢ (n \in ℕ \land m \in ℕ) \to ((((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \land ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1})) \to l = k)$
5	4	rexlimivv	$⊢ \exists n \in ℕ \exists m \in ℕ (((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \land ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1})) \to l = k$
6	1 5	sylbir	$⊢ (\exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \land \exists m \in ℕ ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1})) \to l = k$
7	6	gen2	$⊢ \forall l \forall k ((\exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \land \exists m \in ℕ ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1})) \to l = k)$
8		eqeq1	$⊢ l = k \to (l = [⟨a, b⟩] {Colinear}^{-1} \leftrightarrow k = [⟨a, b⟩] {Colinear}^{-1})$
9	8	anbi2d	$⊢ l = k \to (((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \leftrightarrow ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1}))$
10	9	rexbidv	$⊢ l = k \to (\exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \leftrightarrow \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1}))$
11		fveq2	$⊢ n = m \to 𝔼 (n) = 𝔼 (m)$
12	11	eleq2d	$⊢ n = m \to (a \in 𝔼 (n) \leftrightarrow a \in 𝔼 (m))$
13	11	eleq2d	$⊢ n = m \to (b \in 𝔼 (n) \leftrightarrow b \in 𝔼 (m))$
14	12 13	3anbi12d	$⊢ n = m \to ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \leftrightarrow (a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b))$
15	14	anbi1d	$⊢ n = m \to (((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1}) \leftrightarrow ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1}))$
16	15	cbvrexvw	$⊢ \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1}) \leftrightarrow \exists m \in ℕ ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1})$
17	10 16	bitrdi	$⊢ l = k \to (\exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \leftrightarrow \exists m \in ℕ ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1}))$
18	17	mo4	$⊢ \exists^{*} l \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \leftrightarrow \forall l \forall k ((\exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1}) \land \exists m \in ℕ ((a \in 𝔼 (m) \land b \in 𝔼 (m) \land a \neq b) \land k = [⟨a, b⟩] {Colinear}^{-1})) \to l = k)$
19	7 18	mpbir	$⊢ \exists^{*} l \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})$
20	19	funoprab	$⊢ Fun \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\}$
21		df-line2	$⊢ Line = \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\}$
22	21	funeqi	$⊢ Fun Line \leftrightarrow Fun \{⟨⟨a, b⟩, l⟩ \| \exists n \in ℕ ((a \in 𝔼 (n) \land b \in 𝔼 (n) \land a \neq b) \land l = [⟨a, b⟩] {Colinear}^{-1})\}$
23	20 22	mpbir	$⊢ Fun Line$

Metamath Proof Explorer

Theorem funline

Proof