funray

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

		Ref	Expression
	Assertion	funray	$⊢ Fun Ray$

Proof

Step	Hyp	Ref	Expression
1		reeanv	$⊢ \exists n \in ℕ \exists m \in ℕ (((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \land ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})) \leftrightarrow (\exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \land \exists m \in ℕ ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}))$
2		simp1	$⊢ (p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \to p \in 𝔼 (n)$
3		simp1	$⊢ (p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \to p \in 𝔼 (m)$
4		axdimuniq	$⊢ ((n \in ℕ \land p \in 𝔼 (n)) \land (m \in ℕ \land p \in 𝔼 (m))) \to n = m$
5		fveq2	$⊢ n = m \to 𝔼 (n) = 𝔼 (m)$
6		rabeq	$⊢ 𝔼 (n) = 𝔼 (m) \to \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}$
7	5 6	syl	$⊢ n = m \to \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}$
8	7	eqeq2d	$⊢ n = m \to (r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \leftrightarrow r = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})$
9	8	anbi1d	$⊢ n = m \to ((r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}) \leftrightarrow (r = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\} \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}))$
10		eqtr3	$⊢ (r = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\} \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}) \to r = s$
11	9 10	biimtrdi	$⊢ n = m \to ((r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}) \to r = s)$
12	4 11	syl	$⊢ ((n \in ℕ \land p \in 𝔼 (n)) \land (m \in ℕ \land p \in 𝔼 (m))) \to ((r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}) \to r = s)$
13	12	an4s	$⊢ ((n \in ℕ \land m \in ℕ) \land (p \in 𝔼 (n) \land p \in 𝔼 (m))) \to ((r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}) \to r = s)$
14	13	ex	$⊢ (n \in ℕ \land m \in ℕ) \to ((p \in 𝔼 (n) \land p \in 𝔼 (m)) \to ((r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}) \to r = s))$
15	14	com3l	$⊢ (p \in 𝔼 (n) \land p \in 𝔼 (m)) \to ((r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}) \to ((n \in ℕ \land m \in ℕ) \to r = s))$
16	2 3 15	syl2an	$⊢ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land (p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a)) \to ((r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}) \to ((n \in ℕ \land m \in ℕ) \to r = s))$
17	16	imp	$⊢ (((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land (p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a)) \land (r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})) \to ((n \in ℕ \land m \in ℕ) \to r = s)$
18	17	an4s	$⊢ (((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \land ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})) \to ((n \in ℕ \land m \in ℕ) \to r = s)$
19	18	com12	$⊢ (n \in ℕ \land m \in ℕ) \to ((((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \land ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})) \to r = s)$
20	19	rexlimivv	$⊢ \exists n \in ℕ \exists m \in ℕ (((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \land ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})) \to r = s$
21	1 20	sylbir	$⊢ (\exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \land \exists m \in ℕ ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})) \to r = s$
22	21	gen2	$⊢ \forall r \forall s ((\exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \land \exists m \in ℕ ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})) \to r = s)$
23		eqeq1	$⊢ r = s \to (r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \leftrightarrow s = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\})$
24	23	anbi2d	$⊢ r = s \to (((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \leftrightarrow ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land s = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}))$
25	24	rexbidv	$⊢ r = s \to (\exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \leftrightarrow \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land s = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}))$
26	5	eleq2d	$⊢ n = m \to (p \in 𝔼 (n) \leftrightarrow p \in 𝔼 (m))$
27	5	eleq2d	$⊢ n = m \to (a \in 𝔼 (n) \leftrightarrow a \in 𝔼 (m))$
28	26 27	3anbi12d	$⊢ n = m \to ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \leftrightarrow (p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a))$
29	7	eqeq2d	$⊢ n = m \to (s = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \leftrightarrow s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})$
30	28 29	anbi12d	$⊢ n = m \to (((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land s = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \leftrightarrow ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}))$
31	30	cbvrexvw	$⊢ \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land s = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \leftrightarrow \exists m \in ℕ ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})$
32	25 31	bitrdi	$⊢ r = s \to (\exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \leftrightarrow \exists m \in ℕ ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\}))$
33	32	mo4	$⊢ \exists^{*} r \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \leftrightarrow \forall r \forall s ((\exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}) \land \exists m \in ℕ ((p \in 𝔼 (m) \land a \in 𝔼 (m) \land p \neq a) \land s = \{x \in 𝔼 (m) \| p OutsideOf ⟨a, x⟩\})) \to r = s)$
34	22 33	mpbir	$⊢ \exists^{*} r \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\})$
35	34	funoprab	$⊢ Fun \{⟨⟨p, a⟩, r⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\})\}$
36		df-ray	$⊢ Ray = \{⟨⟨p, a⟩, r⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\})\}$
37	36	funeqi	$⊢ Fun Ray \leftrightarrow Fun \{⟨⟨p, a⟩, r⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\})\}$
38	35 37	mpbir	$⊢ Fun Ray$

Metamath Proof Explorer

Theorem funray

Proof