Metamath Proof Explorer

Theorem rtrclreclem4

Description: The reflexive, transitive closure of R is the smallest reflexive, transitive relation which contains R and the identity. (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 rtrclreclem4 
|- ( ph -> A. s ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) )

Proof

Step Hyp Ref Expression
1 rtrclreclem.1 
 |-  ( ph -> Rel R )
2 eqidd 
 |-  ( ( ph /\ R e. _V ) -> ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) )
3 oveq1 
 |-  ( r = R -> ( r ^r n ) = ( R ^r n ) )
4 3 iuneq2d 
 |-  ( r = R -> U_ n e. NN0 ( r ^r n ) = U_ n e. NN0 ( R ^r n ) )
5 4 adantl 
 |-  ( ( ( ph /\ R e. _V ) /\ r = R ) -> U_ n e. NN0 ( r ^r n ) = U_ n e. NN0 ( R ^r n ) )
6 simpr 
 |-  ( ( ph /\ R e. _V ) -> R e. _V )
7 nn0ex 
 |-  NN0 e. _V
8 ovex 
 |-  ( R ^r n ) e. _V
9 7 8 iunex 
 |-  U_ n e. NN0 ( R ^r n ) e. _V
10 9 a1i 
 |-  ( ( ph /\ R e. _V ) -> U_ n e. NN0 ( R ^r n ) e. _V )
11 2 5 6 10 fvmptd 
 |-  ( ( ph /\ R e. _V ) -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) )
12 eleq1 
 |-  ( i = 0 -> ( i e. NN0 <-> 0 e. NN0 ) )
13 12 anbi1d 
 |-  ( i = 0 -> ( ( i e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) <-> ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) ) )
14 oveq2 
 |-  ( i = 0 -> ( R ^r i ) = ( R ^r 0 ) )
15 14 sseq1d 
 |-  ( i = 0 -> ( ( R ^r i ) C_ s <-> ( R ^r 0 ) C_ s ) )
16 13 15 imbi12d 
 |-  ( i = 0 -> ( ( ( i e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r i ) C_ s ) <-> ( ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r 0 ) C_ s ) ) )
17 eleq1 
 |-  ( i = m -> ( i e. NN0 <-> m e. NN0 ) )
18 17 anbi1d 
 |-  ( i = m -> ( ( i e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) <-> ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) ) )
19 oveq2 
 |-  ( i = m -> ( R ^r i ) = ( R ^r m ) )
20 19 sseq1d 
 |-  ( i = m -> ( ( R ^r i ) C_ s <-> ( R ^r m ) C_ s ) )
21 18 20 imbi12d 
 |-  ( i = m -> ( ( ( i e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r i ) C_ s ) <-> ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) ) )
22 eleq1 
 |-  ( i = ( m + 1 ) -> ( i e. NN0 <-> ( m + 1 ) e. NN0 ) )
23 22 anbi1d 
 |-  ( i = ( m + 1 ) -> ( ( i e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) <-> ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) ) )
24 oveq2 
 |-  ( i = ( m + 1 ) -> ( R ^r i ) = ( R ^r ( m + 1 ) ) )
25 24 sseq1d 
 |-  ( i = ( m + 1 ) -> ( ( R ^r i ) C_ s <-> ( R ^r ( m + 1 ) ) C_ s ) )
26 23 25 imbi12d 
 |-  ( i = ( m + 1 ) -> ( ( ( i e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r i ) C_ s ) <-> ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r ( m + 1 ) ) C_ s ) ) )
27 eleq1 
 |-  ( i = n -> ( i e. NN0 <-> n e. NN0 ) )
28 27 anbi1d 
 |-  ( i = n -> ( ( i e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) <-> ( n e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) ) )
29 oveq2 
 |-  ( i = n -> ( R ^r i ) = ( R ^r n ) )
30 29 sseq1d 
 |-  ( i = n -> ( ( R ^r i ) C_ s <-> ( R ^r n ) C_ s ) )
31 28 30 imbi12d 
 |-  ( i = n -> ( ( ( i e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r i ) C_ s ) <-> ( ( n e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r n ) C_ s ) ) )
32 simprll 
 |-  ( ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ph )
33 32 1 syl 
 |-  ( ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> Rel R )
34 simprlr 
 |-  ( ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> R e. _V )
35 33 34 relexp0d 
 |-  ( ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r 0 ) = ( _I |` U. U. R ) )
36 relfld 
 |-  ( Rel R -> U. U. R = ( dom R u. ran R ) )
37 33 36 syl 
 |-  ( ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> U. U. R = ( dom R u. ran R ) )
38 simprrr 
 |-  ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) -> ( _I |` ( dom R u. ran R ) ) C_ s )
39 38 adantl 
 |-  ( ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( _I |` ( dom R u. ran R ) ) C_ s )
40 reseq2 
 |-  ( U. U. R = ( dom R u. ran R ) -> ( _I |` U. U. R ) = ( _I |` ( dom R u. ran R ) ) )
41 40 sseq1d 
 |-  ( U. U. R = ( dom R u. ran R ) -> ( ( _I |` U. U. R ) C_ s <-> ( _I |` ( dom R u. ran R ) ) C_ s ) )
42 39 41 imbitrrid 
 |-  ( U. U. R = ( dom R u. ran R ) -> ( ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( _I |` U. U. R ) C_ s ) )
43 37 42 mpcom 
 |-  ( ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( _I |` U. U. R ) C_ s )
44 35 43 eqsstrd 
 |-  ( ( 0 e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r 0 ) C_ s )
45 simprrr 
 |-  ( ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) -> m e. NN0 )
46 45 adantl 
 |-  ( ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) -> m e. NN0 )
47 46 adantl 
 |-  ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) -> m e. NN0 )
48 47 adantl 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> m e. NN0 )
49 simprl 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> ( ph /\ R e. _V ) )
50 simprrl 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> ( s o. s ) C_ s )
51 simprrl 
 |-  ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) -> R C_ s )
52 51 adantl 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> R C_ s )
53 simprrl 
 |-  ( ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) -> ( _I |` ( dom R u. ran R ) ) C_ s )
54 53 adantl 
 |-  ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) -> ( _I |` ( dom R u. ran R ) ) C_ s )
55 54 adantl 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> ( _I |` ( dom R u. ran R ) ) C_ s )
56 50 52 55 jca32 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) )
57 48 49 56 jca32 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) )
58 simprrl 
 |-  ( ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) -> ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) )
59 58 adantl 
 |-  ( ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) -> ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) )
60 59 adantl 
 |-  ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) -> ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) )
61 60 adantl 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) )
62 57 61 mpd 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> ( R ^r m ) C_ s )
63 simprll 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> ph )
64 63 adantl 
 |-  ( ( ( R ^r m ) C_ s /\ ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) ) -> ph )
65 64 1 syl 
 |-  ( ( ( R ^r m ) C_ s /\ ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) ) -> Rel R )
66 48 adantl 
 |-  ( ( ( R ^r m ) C_ s /\ ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) ) -> m e. NN0 )
67 65 66 relexpsucrd 
 |-  ( ( ( R ^r m ) C_ s /\ ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) ) -> ( R ^r ( m + 1 ) ) = ( ( R ^r m ) o. R ) )
68 52 adantl 
 |-  ( ( ( R ^r m ) C_ s /\ ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) ) -> R C_ s )
69 coss2 
 |-  ( R C_ s -> ( ( R ^r m ) o. R ) C_ ( ( R ^r m ) o. s ) )
70 68 69 syl 
 |-  ( ( ( R ^r m ) C_ s /\ ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) ) -> ( ( R ^r m ) o. R ) C_ ( ( R ^r m ) o. s ) )
71 coss1 
 |-  ( ( R ^r m ) C_ s -> ( ( R ^r m ) o. s ) C_ ( s o. s ) )
72 71 50 sylan9ss 
 |-  ( ( ( R ^r m ) C_ s /\ ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) ) -> ( ( R ^r m ) o. s ) C_ s )
73 70 72 sstrd 
 |-  ( ( ( R ^r m ) C_ s /\ ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) ) -> ( ( R ^r m ) o. R ) C_ s )
74 67 73 eqsstrd 
 |-  ( ( ( R ^r m ) C_ s /\ ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) ) -> ( R ^r ( m + 1 ) ) C_ s )
75 62 74 mpancom 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) ) -> ( R ^r ( m + 1 ) ) C_ s )
76 75 expcom 
 |-  ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) ) -> ( ( m + 1 ) e. NN0 -> ( R ^r ( m + 1 ) ) C_ s ) )
77 76 expcom 
 |-  ( ( ( s o. s ) C_ s /\ ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) ) -> ( ( ph /\ R e. _V ) -> ( ( m + 1 ) e. NN0 -> ( R ^r ( m + 1 ) ) C_ s ) ) )
78 77 expcom 
 |-  ( ( R C_ s /\ ( ( _I |` ( dom R u. ran R ) ) C_ s /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) -> ( ( s o. s ) C_ s -> ( ( ph /\ R e. _V ) -> ( ( m + 1 ) e. NN0 -> ( R ^r ( m + 1 ) ) C_ s ) ) ) )
79 78 anassrs 
 |-  ( ( ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) -> ( ( s o. s ) C_ s -> ( ( ph /\ R e. _V ) -> ( ( m + 1 ) e. NN0 -> ( R ^r ( m + 1 ) ) C_ s ) ) ) )
80 79 impcom 
 |-  ( ( ( s o. s ) C_ s /\ ( ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) -> ( ( ph /\ R e. _V ) -> ( ( m + 1 ) e. NN0 -> ( R ^r ( m + 1 ) ) C_ s ) ) )
81 80 anassrs 
 |-  ( ( ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) -> ( ( ph /\ R e. _V ) -> ( ( m + 1 ) e. NN0 -> ( R ^r ( m + 1 ) ) C_ s ) ) )
82 81 impcom 
 |-  ( ( ( ph /\ R e. _V ) /\ ( ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) -> ( ( m + 1 ) e. NN0 -> ( R ^r ( m + 1 ) ) C_ s ) )
83 82 anassrs 
 |-  ( ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) -> ( ( m + 1 ) e. NN0 -> ( R ^r ( m + 1 ) ) C_ s ) )
84 83 impcom 
 |-  ( ( ( m + 1 ) e. NN0 /\ ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) ) -> ( R ^r ( m + 1 ) ) C_ s )
85 84 anassrs 
 |-  ( ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) /\ ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) ) -> ( R ^r ( m + 1 ) ) C_ s )
86 85 expcom 
 |-  ( ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) /\ m e. NN0 ) -> ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r ( m + 1 ) ) C_ s ) )
87 86 expcom 
 |-  ( m e. NN0 -> ( ( ( m e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r m ) C_ s ) -> ( ( ( m + 1 ) e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r ( m + 1 ) ) C_ s ) ) )
88 16 21 26 31 44 87 nn0ind 
 |-  ( n e. NN0 -> ( ( n e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r n ) C_ s ) )
89 88 anabsi5 
 |-  ( ( n e. NN0 /\ ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) ) -> ( R ^r n ) C_ s )
90 89 expcom 
 |-  ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) -> ( n e. NN0 -> ( R ^r n ) C_ s ) )
91 90 ralrimiv 
 |-  ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) -> A. n e. NN0 ( R ^r n ) C_ s )
92 iunss 
 |-  ( U_ n e. NN0 ( R ^r n ) C_ s <-> A. n e. NN0 ( R ^r n ) C_ s )
93 91 92 sylibr 
 |-  ( ( ( ph /\ R e. _V ) /\ ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) ) -> U_ n e. NN0 ( R ^r n ) C_ s )
94 93 expcom 
 |-  ( ( ( s o. s ) C_ s /\ ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) ) -> ( ( ph /\ R e. _V ) -> U_ n e. NN0 ( R ^r n ) C_ s ) )
95 94 expcom 
 |-  ( ( R C_ s /\ ( _I |` ( dom R u. ran R ) ) C_ s ) -> ( ( s o. s ) C_ s -> ( ( ph /\ R e. _V ) -> U_ n e. NN0 ( R ^r n ) C_ s ) ) )
96 95 expcom 
 |-  ( ( _I |` ( dom R u. ran R ) ) C_ s -> ( R C_ s -> ( ( s o. s ) C_ s -> ( ( ph /\ R e. _V ) -> U_ n e. NN0 ( R ^r n ) C_ s ) ) ) )
97 96 3imp1 
 |-  ( ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) /\ ( ph /\ R e. _V ) ) -> U_ n e. NN0 ( R ^r n ) C_ s )
98 97 expcom 
 |-  ( ( ph /\ R e. _V ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> U_ n e. NN0 ( R ^r n ) C_ s ) )
99 sseq1 
 |-  ( ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) -> ( ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) C_ s <-> U_ n e. NN0 ( R ^r n ) C_ s ) )
100 99 imbi2d 
 |-  ( ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) -> ( ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) C_ s ) <-> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> U_ n e. NN0 ( R ^r n ) C_ s ) ) )
101 98 100 imbitrrid 
 |-  ( ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) -> ( ( ph /\ R e. _V ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) C_ s ) ) )
102 11 101 mpcom 
 |-  ( ( ph /\ R e. _V ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) C_ s ) )
103 df-rtrclrec 
 |-  t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )
104 fveq1 
 |-  ( t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) -> ( t*rec ` R ) = ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) )
105 104 sseq1d 
 |-  ( t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) -> ( ( t*rec ` R ) C_ s <-> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) C_ s ) )
106 105 imbi2d 
 |-  ( t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) -> ( ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) <-> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) C_ s ) ) )
107 106 imbi2d 
 |-  ( t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) -> ( ( ( ph /\ R e. _V ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) ) <-> ( ( ph /\ R e. _V ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) C_ s ) ) ) )
108 103 107 ax-mp 
 |-  ( ( ( ph /\ R e. _V ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) ) <-> ( ( ph /\ R e. _V ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) C_ s ) ) )
109 102 108 mpbir 
 |-  ( ( ph /\ R e. _V ) -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) )
110 109 ex 
 |-  ( ph -> ( R e. _V -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) ) )
111 fvprc 
 |-  ( -. R e. _V -> ( t*rec ` R ) = (/) )
112 0ss 
 |-  (/) C_ s
113 111 112 eqsstrdi 
 |-  ( -. R e. _V -> ( t*rec ` R ) C_ s )
114 113 a1d 
 |-  ( -. R e. _V -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) )
115 110 114 pm2.61d1 
 |-  ( ph -> ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) )
116 115 alrimiv 
 |-  ( ph -> A. s ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) )