Metamath Proof Explorer


Theorem 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 n m p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x m p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x
2 simp1 p 𝔼 n a 𝔼 n p a p 𝔼 n
3 simp1 p 𝔼 m a 𝔼 m p a p 𝔼 m
4 axdimuniq n p 𝔼 n m p 𝔼 m n = m
5 fveq2 n = m 𝔼 n = 𝔼 m
6 rabeq 𝔼 n = 𝔼 m x 𝔼 n | p OutsideOf a x = x 𝔼 m | p OutsideOf a x
7 5 6 syl n = m x 𝔼 n | p OutsideOf a x = x 𝔼 m | p OutsideOf a x
8 7 eqeq2d n = m r = x 𝔼 n | p OutsideOf a x r = x 𝔼 m | p OutsideOf a x
9 8 anbi1d n = m r = x 𝔼 n | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x r = x 𝔼 m | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x
10 eqtr3 r = x 𝔼 m | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x r = s
11 9 10 syl6bi n = m r = x 𝔼 n | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x r = s
12 4 11 syl n p 𝔼 n m p 𝔼 m r = x 𝔼 n | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x r = s
13 12 an4s n m p 𝔼 n p 𝔼 m r = x 𝔼 n | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x r = s
14 13 ex n m p 𝔼 n p 𝔼 m r = x 𝔼 n | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x r = s
15 14 com3l p 𝔼 n p 𝔼 m r = x 𝔼 n | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x n m r = s
16 2 3 15 syl2an p 𝔼 n a 𝔼 n p a p 𝔼 m a 𝔼 m p a r = x 𝔼 n | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x n m r = s
17 16 imp p 𝔼 n a 𝔼 n p a p 𝔼 m a 𝔼 m p a r = x 𝔼 n | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x n m r = s
18 17 an4s p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x n m r = s
19 18 com12 n m p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x r = s
20 19 rexlimivv n m p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x r = s
21 1 20 sylbir n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x m p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x r = s
22 21 gen2 r s n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x m p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x r = s
23 eqeq1 r = s r = x 𝔼 n | p OutsideOf a x s = x 𝔼 n | p OutsideOf a x
24 23 anbi2d r = s p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x p 𝔼 n a 𝔼 n p a s = x 𝔼 n | p OutsideOf a x
25 24 rexbidv r = s n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x n p 𝔼 n a 𝔼 n p a s = x 𝔼 n | p OutsideOf a x
26 5 eleq2d n = m p 𝔼 n p 𝔼 m
27 5 eleq2d n = m a 𝔼 n a 𝔼 m
28 26 27 3anbi12d n = m p 𝔼 n a 𝔼 n p a p 𝔼 m a 𝔼 m p a
29 7 eqeq2d n = m s = x 𝔼 n | p OutsideOf a x s = x 𝔼 m | p OutsideOf a x
30 28 29 anbi12d n = m p 𝔼 n a 𝔼 n p a s = x 𝔼 n | p OutsideOf a x p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x
31 30 cbvrexvw n p 𝔼 n a 𝔼 n p a s = x 𝔼 n | p OutsideOf a x m p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x
32 25 31 bitrdi r = s n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x m p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x
33 32 mo4 * r n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x r s n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x m p 𝔼 m a 𝔼 m p a s = x 𝔼 m | p OutsideOf a x r = s
34 22 33 mpbir * r n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x
35 34 funoprab Fun p a r | n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x
36 df-ray Ray = p a r | n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x
37 36 funeqi Fun Ray Fun p a r | n p 𝔼 n a 𝔼 n p a r = x 𝔼 n | p OutsideOf a x
38 35 37 mpbir Fun Ray