Metamath Proof Explorer

Theorem rtrclreclem3

Description: The reflexive, transitive closure is indeed transitive. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 13-Jul-2024)

Ref Expression
Hypothesis rtrclreclem.1 
|- ( ph -> Rel R )
Assertion rtrclreclem3 
|- ( ph -> ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) )

Proof

Step Hyp Ref Expression
1 rtrclreclem.1 
 |-  ( ph -> Rel R )
2 df-co 
 |-  ( ( t*rec ` R ) o. ( t*rec ` R ) ) = { <. e , g >. | E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) }
3 elopab 
 |-  ( d e. { <. e , g >. | E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) } <-> E. e E. g ( d = <. e , g >. /\ E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) ) )
4 eqeq1 
 |-  ( d = <. e , g >. -> ( d = <. e , g >. <-> <. e , g >. = <. e , g >. ) )
5 4 anbi1d 
 |-  ( d = <. e , g >. -> ( ( d = <. e , g >. /\ ( E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) /\ ph ) ) <-> ( <. e , g >. = <. e , g >. /\ ( E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) /\ ph ) ) ) )
6 simprr 
 |-  ( ( <. e , g >. = <. e , g >. /\ ( E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) /\ ph ) ) -> ph )
7 simprl 
 |-  ( ( <. e , g >. = <. e , g >. /\ ( E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) /\ ph ) ) -> E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) )
8 simpl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ph ) ) -> e ( t*rec ` R ) f )
9 simprr 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ph ) ) -> ph )
10 1 dfrtrclrec2 
 |-  ( ph -> ( e ( t*rec ` R ) f <-> E. n e. NN0 e ( R ^r n ) f ) )
11 9 10 syl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ph ) ) -> ( e ( t*rec ` R ) f <-> E. n e. NN0 e ( R ^r n ) f ) )
12 8 11 mpbid 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ph ) ) -> E. n e. NN0 e ( R ^r n ) f )
13 simprl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) ) -> f ( t*rec ` R ) g )
14 simprrl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) ) -> ph )
15 1 dfrtrclrec2 
 |-  ( ph -> ( f ( t*rec ` R ) g <-> E. m e. NN0 f ( R ^r m ) g ) )
16 14 15 syl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) ) -> ( f ( t*rec ` R ) g <-> E. m e. NN0 f ( R ^r m ) g ) )
17 13 16 mpbid 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) ) -> E. m e. NN0 f ( R ^r m ) g )
18 simprrl 
 |-  ( ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) -> n e. NN0 )
19 18 adantl 
 |-  ( ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) -> n e. NN0 )
20 19 adantl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> n e. NN0 )
21 simprr 
 |-  ( ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) -> m e. NN0 )
22 21 adantl 
 |-  ( ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) -> m e. NN0 )
23 22 adantl 
 |-  ( ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) -> m e. NN0 )
24 23 adantl 
 |-  ( ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) -> m e. NN0 )
25 24 adantl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> m e. NN0 )
26 20 25 nn0addcld 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> ( n + m ) e. NN0 )
27 20 adantl 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> n e. NN0 )
28 27 nn0cnd 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> n e. CC )
29 25 adantl 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> m e. NN0 )
30 29 nn0cnd 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> m e. CC )
31 28 30 addcomd 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> ( n + m ) = ( m + n ) )
32 eleq1 
 |-  ( ( n + m ) = ( m + n ) -> ( ( n + m ) e. NN0 <-> ( m + n ) e. NN0 ) )
33 32 anbi1d 
 |-  ( ( n + m ) = ( m + n ) -> ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) <-> ( ( m + n ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) ) )
34 simprrl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> ph )
35 34 adantl 
 |-  ( ( ( m + n ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> ph )
36 35 1 syl 
 |-  ( ( ( m + n ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> Rel R )
37 25 adantl 
 |-  ( ( ( m + n ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> m e. NN0 )
38 20 adantl 
 |-  ( ( ( m + n ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> n e. NN0 )
39 36 37 38 relexpaddd 
 |-  ( ( ( m + n ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> ( ( R ^r m ) o. ( R ^r n ) ) = ( R ^r ( m + n ) ) )
40 oveq2 
 |-  ( ( n + m ) = ( m + n ) -> ( R ^r ( n + m ) ) = ( R ^r ( m + n ) ) )
41 40 eqeq2d 
 |-  ( ( n + m ) = ( m + n ) -> ( ( ( R ^r m ) o. ( R ^r n ) ) = ( R ^r ( n + m ) ) <-> ( ( R ^r m ) o. ( R ^r n ) ) = ( R ^r ( m + n ) ) ) )
42 39 41 syl5ibr 
 |-  ( ( n + m ) = ( m + n ) -> ( ( ( m + n ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> ( ( R ^r m ) o. ( R ^r n ) ) = ( R ^r ( n + m ) ) ) )
43 33 42 sylbid 
 |-  ( ( n + m ) = ( m + n ) -> ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> ( ( R ^r m ) o. ( R ^r n ) ) = ( R ^r ( n + m ) ) ) )
44 31 43 mpcom 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> ( ( R ^r m ) o. ( R ^r n ) ) = ( R ^r ( n + m ) ) )
45 simprrl 
 |-  ( ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) -> e ( R ^r n ) f )
46 45 adantl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> e ( R ^r n ) f )
47 simprrl 
 |-  ( ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) -> f ( R ^r m ) g )
48 47 adantl 
 |-  ( ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) -> f ( R ^r m ) g )
49 48 adantl 
 |-  ( ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) -> f ( R ^r m ) g )
50 49 adantl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> f ( R ^r m ) g )
51 50 adantl 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> f ( R ^r m ) g )
52 vex 
 |-  f e. _V
53 breq2 
 |-  ( h = f -> ( e ( R ^r n ) h <-> e ( R ^r n ) f ) )
54 breq1 
 |-  ( h = f -> ( h ( R ^r m ) g <-> f ( R ^r m ) g ) )
55 53 54 anbi12d 
 |-  ( h = f -> ( ( e ( R ^r n ) h /\ h ( R ^r m ) g ) <-> ( e ( R ^r n ) f /\ f ( R ^r m ) g ) ) )
56 52 55 spcev 
 |-  ( ( e ( R ^r n ) f /\ f ( R ^r m ) g ) -> E. h ( e ( R ^r n ) h /\ h ( R ^r m ) g ) )
57 46 51 56 syl2an2 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> E. h ( e ( R ^r n ) h /\ h ( R ^r m ) g ) )
58 vex 
 |-  e e. _V
59 vex 
 |-  g e. _V
60 58 59 brco 
 |-  ( e ( ( R ^r m ) o. ( R ^r n ) ) g <-> E. h ( e ( R ^r n ) h /\ h ( R ^r m ) g ) )
61 57 60 sylibr 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> e ( ( R ^r m ) o. ( R ^r n ) ) g )
62 44 61 breqdi 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> e ( R ^r ( n + m ) ) g )
63 oveq2 
 |-  ( i = ( n + m ) -> ( R ^r i ) = ( R ^r ( n + m ) ) )
64 63 breqd 
 |-  ( i = ( n + m ) -> ( e ( R ^r i ) g <-> e ( R ^r ( n + m ) ) g ) )
65 64 rspcev 
 |-  ( ( ( n + m ) e. NN0 /\ e ( R ^r ( n + m ) ) g ) -> E. i e. NN0 e ( R ^r i ) g )
66 62 65 syldan 
 |-  ( ( ( n + m ) e. NN0 /\ ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) ) -> E. i e. NN0 e ( R ^r i ) g )
67 26 66 mpancom 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> E. i e. NN0 e ( R ^r i ) g )
68 df-br 
 |-  ( e ( t*rec ` R ) g <-> <. e , g >. e. ( t*rec ` R ) )
69 34 1 syl 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> Rel R )
70 69 dfrtrclrec2 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> ( e ( t*rec ` R ) g <-> E. i e. NN0 e ( R ^r i ) g ) )
71 68 70 bitr3id 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> ( <. e , g >. e. ( t*rec ` R ) <-> E. i e. NN0 e ( R ^r i ) g ) )
72 67 71 mpbird 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) ) -> <. e , g >. e. ( t*rec ` R ) )
73 72 expcom 
 |-  ( ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) ) -> ( e ( t*rec ` R ) f -> <. e , g >. e. ( t*rec ` R ) ) )
74 73 expcom 
 |-  ( ( ph /\ ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) ) -> ( f ( t*rec ` R ) g -> ( e ( t*rec ` R ) f -> <. e , g >. e. ( t*rec ` R ) ) ) )
75 74 expcom 
 |-  ( ( e ( R ^r n ) f /\ ( n e. NN0 /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) -> ( ph -> ( f ( t*rec ` R ) g -> ( e ( t*rec ` R ) f -> <. e , g >. e. ( t*rec ` R ) ) ) ) )
76 75 anassrs 
 |-  ( ( ( e ( R ^r n ) f /\ n e. NN0 ) /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) -> ( ph -> ( f ( t*rec ` R ) g -> ( e ( t*rec ` R ) f -> <. e , g >. e. ( t*rec ` R ) ) ) ) )
77 76 impcom 
 |-  ( ( ph /\ ( ( e ( R ^r n ) f /\ n e. NN0 ) /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) -> ( f ( t*rec ` R ) g -> ( e ( t*rec ` R ) f -> <. e , g >. e. ( t*rec ` R ) ) ) )
78 77 anassrs 
 |-  ( ( ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) -> ( f ( t*rec ` R ) g -> ( e ( t*rec ` R ) f -> <. e , g >. e. ( t*rec ` R ) ) ) )
79 78 impcom 
 |-  ( ( f ( t*rec ` R ) g /\ ( ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) -> ( e ( t*rec ` R ) f -> <. e , g >. e. ( t*rec ` R ) ) )
80 79 anassrs 
 |-  ( ( ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) -> ( e ( t*rec ` R ) f -> <. e , g >. e. ( t*rec ` R ) ) )
81 80 impcom 
 |-  ( ( e ( t*rec ` R ) f /\ ( ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) ) -> <. e , g >. e. ( t*rec ` R ) )
82 81 anassrs 
 |-  ( ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) ) /\ ( f ( R ^r m ) g /\ m e. NN0 ) ) -> <. e , g >. e. ( t*rec ` R ) )
83 82 expcom 
 |-  ( ( f ( R ^r m ) g /\ m e. NN0 ) -> ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) ) -> <. e , g >. e. ( t*rec ` R ) ) )
84 83 expcom 
 |-  ( m e. NN0 -> ( f ( R ^r m ) g -> ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) ) -> <. e , g >. e. ( t*rec ` R ) ) ) )
85 84 rexlimiv 
 |-  ( E. m e. NN0 f ( R ^r m ) g -> ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) ) -> <. e , g >. e. ( t*rec ` R ) ) )
86 17 85 mpcom 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) ) -> <. e , g >. e. ( t*rec ` R ) )
87 86 expcom 
 |-  ( ( f ( t*rec ` R ) g /\ ( ph /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) -> ( e ( t*rec ` R ) f -> <. e , g >. e. ( t*rec ` R ) ) )
88 87 anassrs 
 |-  ( ( ( f ( t*rec ` R ) g /\ ph ) /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) -> ( e ( t*rec ` R ) f -> <. e , g >. e. ( t*rec ` R ) ) )
89 88 impcom 
 |-  ( ( e ( t*rec ` R ) f /\ ( ( f ( t*rec ` R ) g /\ ph ) /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) ) -> <. e , g >. e. ( t*rec ` R ) )
90 89 anassrs 
 |-  ( ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ph ) ) /\ ( e ( R ^r n ) f /\ n e. NN0 ) ) -> <. e , g >. e. ( t*rec ` R ) )
91 90 expcom 
 |-  ( ( e ( R ^r n ) f /\ n e. NN0 ) -> ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ph ) ) -> <. e , g >. e. ( t*rec ` R ) ) )
92 91 expcom 
 |-  ( n e. NN0 -> ( e ( R ^r n ) f -> ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ph ) ) -> <. e , g >. e. ( t*rec ` R ) ) ) )
93 92 rexlimiv 
 |-  ( E. n e. NN0 e ( R ^r n ) f -> ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ph ) ) -> <. e , g >. e. ( t*rec ` R ) ) )
94 12 93 mpcom 
 |-  ( ( e ( t*rec ` R ) f /\ ( f ( t*rec ` R ) g /\ ph ) ) -> <. e , g >. e. ( t*rec ` R ) )
95 94 anassrs 
 |-  ( ( ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) /\ ph ) -> <. e , g >. e. ( t*rec ` R ) )
96 95 expcom 
 |-  ( ph -> ( ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) -> <. e , g >. e. ( t*rec ` R ) ) )
97 96 exlimdv 
 |-  ( ph -> ( E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) -> <. e , g >. e. ( t*rec ` R ) ) )
98 6 7 97 sylc 
 |-  ( ( <. e , g >. = <. e , g >. /\ ( E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) /\ ph ) ) -> <. e , g >. e. ( t*rec ` R ) )
99 eleq1 
 |-  ( d = <. e , g >. -> ( d e. ( t*rec ` R ) <-> <. e , g >. e. ( t*rec ` R ) ) )
100 98 99 syl5ibr 
 |-  ( d = <. e , g >. -> ( ( <. e , g >. = <. e , g >. /\ ( E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) /\ ph ) ) -> d e. ( t*rec ` R ) ) )
101 5 100 sylbid 
 |-  ( d = <. e , g >. -> ( ( d = <. e , g >. /\ ( E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) /\ ph ) ) -> d e. ( t*rec ` R ) ) )
102 101 anabsi5 
 |-  ( ( d = <. e , g >. /\ ( E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) /\ ph ) ) -> d e. ( t*rec ` R ) )
103 102 anassrs 
 |-  ( ( ( d = <. e , g >. /\ E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) ) /\ ph ) -> d e. ( t*rec ` R ) )
104 103 expcom 
 |-  ( ph -> ( ( d = <. e , g >. /\ E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) ) -> d e. ( t*rec ` R ) ) )
105 104 exlimdvv 
 |-  ( ph -> ( E. e E. g ( d = <. e , g >. /\ E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) ) -> d e. ( t*rec ` R ) ) )
106 3 105 syl5bi 
 |-  ( ph -> ( d e. { <. e , g >. | E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) } -> d e. ( t*rec ` R ) ) )
107 eleq2 
 |-  ( ( ( t*rec ` R ) o. ( t*rec ` R ) ) = { <. e , g >. | E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) } -> ( d e. ( ( t*rec ` R ) o. ( t*rec ` R ) ) <-> d e. { <. e , g >. | E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) } ) )
108 107 imbi1d 
 |-  ( ( ( t*rec ` R ) o. ( t*rec ` R ) ) = { <. e , g >. | E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) } -> ( ( d e. ( ( t*rec ` R ) o. ( t*rec ` R ) ) -> d e. ( t*rec ` R ) ) <-> ( d e. { <. e , g >. | E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) } -> d e. ( t*rec ` R ) ) ) )
109 106 108 syl5ibr 
 |-  ( ( ( t*rec ` R ) o. ( t*rec ` R ) ) = { <. e , g >. | E. f ( e ( t*rec ` R ) f /\ f ( t*rec ` R ) g ) } -> ( ph -> ( d e. ( ( t*rec ` R ) o. ( t*rec ` R ) ) -> d e. ( t*rec ` R ) ) ) )
110 2 109 ax-mp 
 |-  ( ph -> ( d e. ( ( t*rec ` R ) o. ( t*rec ` R ) ) -> d e. ( t*rec ` R ) ) )
111 110 ssrdv 
 |-  ( ph -> ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) )