fvray

Description: Calculate the value of the Ray function. (Contributed by Scott Fenton, 21-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	fvray	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A)) \to P Ray A = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}$

Proof

Step	Hyp	Ref	Expression
1		df-ov	$⊢ P Ray A = Ray (⟨P, A⟩)$
2		eqid	$⊢ \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}$
3		fveq2	$⊢ n = N \to 𝔼 (n) = 𝔼 (N)$
4	3	eleq2d	$⊢ n = N \to (P \in 𝔼 (n) \leftrightarrow P \in 𝔼 (N))$
5	3	eleq2d	$⊢ n = N \to (A \in 𝔼 (n) \leftrightarrow A \in 𝔼 (N))$
6	4 5	3anbi12d	$⊢ n = N \to ((P \in 𝔼 (n) \land A \in 𝔼 (n) \land P \neq A) \leftrightarrow (P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A))$
7		rabeq	$⊢ 𝔼 (n) = 𝔼 (N) \to \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}$
8	3 7	syl	$⊢ n = N \to \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}$
9	8	eqeq2d	$⊢ n = N \to (\{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\} \leftrightarrow \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\})$
10	6 9	anbi12d	$⊢ n = N \to (((P \in 𝔼 (n) \land A \in 𝔼 (n) \land P \neq A) \land \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\}) \leftrightarrow ((P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A) \land \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}))$
11	10	rspcev	$⊢ (N \in ℕ \land ((P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A) \land \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\})) \to \exists n \in ℕ ((P \in 𝔼 (n) \land A \in 𝔼 (n) \land P \neq A) \land \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\})$
12	2 11	mpanr2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A)) \to \exists n \in ℕ ((P \in 𝔼 (n) \land A \in 𝔼 (n) \land P \neq A) \land \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\})$
13		simpr1	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A)) \to P \in 𝔼 (N)$
14		simpr2	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A)) \to A \in 𝔼 (N)$
15		fvex	$⊢ 𝔼 (N) \in V$
16	15	rabex	$⊢ \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} \in V$
17		eleq1	$⊢ p = P \to (p \in 𝔼 (n) \leftrightarrow P \in 𝔼 (n))$
18		neeq1	$⊢ p = P \to (p \neq a \leftrightarrow P \neq a)$
19	17 18	3anbi13d	$⊢ p = P \to ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \leftrightarrow (P \in 𝔼 (n) \land a \in 𝔼 (n) \land P \neq a))$
20		breq1	$⊢ p = P \to (p OutsideOf ⟨a, x⟩ \leftrightarrow P OutsideOf ⟨a, x⟩)$
21	20	rabbidv	$⊢ p = P \to \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨a, x⟩\}$
22	21	eqeq2d	$⊢ p = P \to (r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\} \leftrightarrow r = \{x \in 𝔼 (n) \| P OutsideOf ⟨a, x⟩\})$
23	19 22	anbi12d	$⊢ p = P \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 r = \{x \in 𝔼 (n) \| P OutsideOf ⟨a, x⟩\}))$
24	23	rexbidv	$⊢ p = P \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 r = \{x \in 𝔼 (n) \| P OutsideOf ⟨a, x⟩\}))$
25		eleq1	$⊢ a = A \to (a \in 𝔼 (n) \leftrightarrow A \in 𝔼 (n))$
26		neeq2	$⊢ a = A \to (P \neq a \leftrightarrow P \neq A)$
27	25 26	3anbi23d	$⊢ a = A \to ((P \in 𝔼 (n) \land a \in 𝔼 (n) \land P \neq a) \leftrightarrow (P \in 𝔼 (n) \land A \in 𝔼 (n) \land P \neq A))$
28		opeq1	$⊢ a = A \to ⟨a, x⟩ = ⟨A, x⟩$
29	28	breq2d	$⊢ a = A \to (P OutsideOf ⟨a, x⟩ \leftrightarrow P OutsideOf ⟨A, x⟩)$
30	29	rabbidv	$⊢ a = A \to \{x \in 𝔼 (n) \| P OutsideOf ⟨a, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\}$
31	30	eqeq2d	$⊢ a = A \to (r = \{x \in 𝔼 (n) \| P OutsideOf ⟨a, x⟩\} \leftrightarrow r = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\})$
32	27 31	anbi12d	$⊢ a = A \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 r = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\}))$
33	32	rexbidv	$⊢ a = A \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 r = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\}))$
34		eqeq1	$⊢ r = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} \to (r = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\} \leftrightarrow \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\})$
35	34	anbi2d	$⊢ r = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} \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 \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\}))$
36	35	rexbidv	$⊢ r = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} \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 \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\}))$
37	24 33 36	eloprabg	$⊢ (P \in 𝔼 (N) \land A \in 𝔼 (N) \land \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} \in V) \to (⟨⟨P, A⟩, \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}⟩ \in \{⟨⟨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⟩\})\} \leftrightarrow \exists n \in ℕ ((P \in 𝔼 (n) \land A \in 𝔼 (n) \land P \neq A) \land \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\}))$
38	16 37	mp3an3	$⊢ (P \in 𝔼 (N) \land A \in 𝔼 (N)) \to (⟨⟨P, A⟩, \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}⟩ \in \{⟨⟨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⟩\})\} \leftrightarrow \exists n \in ℕ ((P \in 𝔼 (n) \land A \in 𝔼 (n) \land P \neq A) \land \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\}))$
39	13 14 38	syl2anc	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A)) \to (⟨⟨P, A⟩, \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}⟩ \in \{⟨⟨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⟩\})\} \leftrightarrow \exists n \in ℕ ((P \in 𝔼 (n) \land A \in 𝔼 (n) \land P \neq A) \land \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} = \{x \in 𝔼 (n) \| P OutsideOf ⟨A, x⟩\}))$
40	12 39	mpbird	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A)) \to ⟨⟨P, A⟩, \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}⟩ \in \{⟨⟨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⟩\})\}$
41		df-br	$⊢ ⟨P, A⟩ Ray \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} \leftrightarrow ⟨⟨P, A⟩, \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}⟩ \in Ray$
42		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⟩\})\}$
43	42	eleq2i	$⊢ ⟨⟨P, A⟩, \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}⟩ \in Ray \leftrightarrow ⟨⟨P, A⟩, \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}⟩ \in \{⟨⟨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⟩\})\}$
44	41 43	bitri	$⊢ ⟨P, A⟩ Ray \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} \leftrightarrow ⟨⟨P, A⟩, \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}⟩ \in \{⟨⟨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⟩\})\}$
45		funray	$⊢ Fun Ray$
46		funbrfv	$⊢ Fun Ray \to (⟨P, A⟩ Ray \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} \to Ray (⟨P, A⟩) = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\})$
47	45 46	ax-mp	$⊢ ⟨P, A⟩ Ray \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\} \to Ray (⟨P, A⟩) = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}$
48	44 47	sylbir	$⊢ ⟨⟨P, A⟩, \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}⟩ \in \{⟨⟨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⟩\})\} \to Ray (⟨P, A⟩) = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}$
49	40 48	syl	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A)) \to Ray (⟨P, A⟩) = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}$
50	1 49	syl5eq	$⊢ (N \in ℕ \land (P \in 𝔼 (N) \land A \in 𝔼 (N) \land P \neq A)) \to P Ray A = \{x \in 𝔼 (N) \| P OutsideOf ⟨A, x⟩\}$

Metamath Proof Explorer

Theorem fvray

Proof