Metamath Proof Explorer

Theorem rtrclreclem1

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

Ref Expression
Hypothesis rtrclreclem1.1 
|- ( ph -> R e. V )
Assertion rtrclreclem1 
|- ( ph -> R C_ ( t*rec ` R ) )

Proof

Step Hyp Ref Expression
1 rtrclreclem1.1 
 |-  ( ph -> R e. V )
2 1nn0 
 |-  1 e. NN0
3 ssidd 
 |-  ( ph -> R C_ R )
4 1 relexp1d 
 |-  ( ph -> ( R ^r 1 ) = R )
5 3 4 sseqtrrd 
 |-  ( ph -> R C_ ( R ^r 1 ) )
6 oveq2 
 |-  ( n = 1 -> ( R ^r n ) = ( R ^r 1 ) )
7 6 sseq2d 
 |-  ( n = 1 -> ( R C_ ( R ^r n ) <-> R C_ ( R ^r 1 ) ) )
8 7 rspcev 
 |-  ( ( 1 e. NN0 /\ R C_ ( R ^r 1 ) ) -> E. n e. NN0 R C_ ( R ^r n ) )
9 2 5 8 sylancr 
 |-  ( ph -> E. n e. NN0 R C_ ( R ^r n ) )
10 ssiun 
 |-  ( E. n e. NN0 R C_ ( R ^r n ) -> R C_ U_ n e. NN0 ( R ^r n ) )
11 9 10 syl 
 |-  ( ph -> R C_ U_ n e. NN0 ( R ^r n ) )
12 eqidd 
 |-  ( ph -> ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) )
13 oveq1 
 |-  ( r = R -> ( r ^r n ) = ( R ^r n ) )
14 13 iuneq2d 
 |-  ( r = R -> U_ n e. NN0 ( r ^r n ) = U_ n e. NN0 ( R ^r n ) )
15 14 adantl 
 |-  ( ( ph /\ r = R ) -> U_ n e. NN0 ( r ^r n ) = U_ n e. NN0 ( R ^r n ) )
16 1 elexd 
 |-  ( ph -> R e. _V )
17 nn0ex 
 |-  NN0 e. _V
18 ovex 
 |-  ( R ^r n ) e. _V
19 17 18 iunex 
 |-  U_ n e. NN0 ( R ^r n ) e. _V
20 19 a1i 
 |-  ( ph -> U_ n e. NN0 ( R ^r n ) e. _V )
21 12 15 16 20 fvmptd 
 |-  ( ph -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) )
22 11 21 sseqtrrd 
 |-  ( ph -> 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 ) ) -> ( R C_ ( t*rec ` R ) <-> 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 -> R C_ ( t*rec ` R ) ) <-> ( ph -> R C_ ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) ) ) )
27 23 26 ax-mp 
 |-  ( ( ph -> R C_ ( t*rec ` R ) ) <-> ( ph -> R C_ ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) ) )
28 22 27 mpbir 
 |-  ( ph -> R C_ ( t*rec ` R ) )