Metamath Proof Explorer

Theorem rtrclreclem2

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

Ref Expression
Hypotheses rtrclreclem2.1 
|- ( ph -> Rel R )
rtrclreclem2.2 
|- ( ph -> R e. V )
Assertion rtrclreclem2 
|- ( ph -> ( _I |` U. U. R ) C_ ( t*rec ` R ) )

Proof

Step Hyp Ref Expression
1 rtrclreclem2.1 
 |-  ( ph -> Rel R )
2 rtrclreclem2.2 
 |-  ( ph -> R e. V )
3 0nn0 
 |-  0 e. NN0
4 ssid 
 |-  ( _I |` U. U. R ) C_ ( _I |` U. U. R )
5 1 2 relexp0d 
 |-  ( ph -> ( R ^r 0 ) = ( _I |` U. U. R ) )
6 4 5 sseqtrrid 
 |-  ( ph -> ( _I |` U. U. R ) C_ ( R ^r 0 ) )
7 oveq2 
 |-  ( n = 0 -> ( R ^r n ) = ( R ^r 0 ) )
8 7 sseq2d 
 |-  ( n = 0 -> ( ( _I |` U. U. R ) C_ ( R ^r n ) <-> ( _I |` U. U. R ) C_ ( R ^r 0 ) ) )
9 8 rspcev 
 |-  ( ( 0 e. NN0 /\ ( _I |` U. U. R ) C_ ( R ^r 0 ) ) -> E. n e. NN0 ( _I |` U. U. R ) C_ ( R ^r n ) )
10 3 6 9 sylancr 
 |-  ( ph -> E. n e. NN0 ( _I |` U. U. R ) C_ ( R ^r n ) )
11 ssiun 
 |-  ( E. n e. NN0 ( _I |` U. U. R ) C_ ( R ^r n ) -> ( _I |` U. U. R ) C_ U_ n e. NN0 ( R ^r n ) )
12 10 11 syl 
 |-  ( ph -> ( _I |` U. U. R ) C_ U_ n e. NN0 ( R ^r n ) )
13 2 elexd 
 |-  ( ph -> R e. _V )
14 nn0ex 
 |-  NN0 e. _V
15 ovex 
 |-  ( R ^r n ) e. _V
16 14 15 iunex 
 |-  U_ n e. NN0 ( R ^r n ) e. _V
17 oveq1 
 |-  ( r = R -> ( r ^r n ) = ( R ^r n ) )
18 17 iuneq2d 
 |-  ( r = R -> U_ n e. NN0 ( r ^r n ) = U_ n e. NN0 ( R ^r n ) )
19 eqid 
 |-  ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )
20 18 19 fvmptg 
 |-  ( ( R e. _V /\ U_ n e. NN0 ( R ^r n ) e. _V ) -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) )
21 13 16 20 sylancl 
 |-  ( ph -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) )
22 12 21 sseqtrrd 
 |-  ( ph -> ( _I |` U. U. R ) C_ ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) )
23 df-rtrclrec 
 |-  t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )
24 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 ) )
25 24 sseq2d 
 |-  ( t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) -> ( ( _I |` U. U. R ) C_ ( t*rec ` R ) <-> ( _I |` U. U. R ) C_ ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) ) )
26 25 imbi2d 
 |-  ( t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) -> ( ( ph -> ( _I |` U. U. R ) C_ ( t*rec ` R ) ) <-> ( ph -> ( _I |` U. U. R ) C_ ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) ) ) )
27 23 26 ax-mp 
 |-  ( ( ph -> ( _I |` U. U. R ) C_ ( t*rec ` R ) ) <-> ( ph -> ( _I |` U. U. R ) C_ ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) ) )
28 22 27 mpbir 
 |-  ( ph -> ( _I |` U. U. R ) C_ ( t*rec ` R ) )