Metamath Proof Explorer

Theorem 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 e. NN /\ ( P e. ( EE ` N ) /\ A e. ( EE ` N ) /\ P =/= A ) ) -> ( P Ray A ) = { x e. ( EE ` N ) | P OutsideOf <. A , x >. } )

Proof

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