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