Metamath Proof Explorer

Theorem dfrtrclrec2

Description: If two elements are connected by a reflexive, transitive closure, then they are connected via n instances the relation, for some n . (Contributed by Drahflow, 12-Nov-2015) (Revised by AV, 13-Jul-2024)

Ref Expression
Hypothesis dfrtrclrec2.1 
|- ( ph -> Rel R )
Assertion dfrtrclrec2 
|- ( ph -> ( A ( t*rec ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) )

Proof

Step Hyp Ref Expression
1 dfrtrclrec2.1 
 |-  ( ph -> Rel R )
2 simpr 
 |-  ( ( ph /\ R e. _V ) -> R e. _V )
3 nn0ex 
 |-  NN0 e. _V
4 ovex 
 |-  ( R ^r n ) e. _V
5 3 4 iunex 
 |-  U_ n e. NN0 ( R ^r n ) e. _V
6 oveq1 
 |-  ( r = R -> ( r ^r n ) = ( R ^r n ) )
7 6 iuneq2d 
 |-  ( r = R -> U_ n e. NN0 ( r ^r n ) = U_ n e. NN0 ( R ^r n ) )
8 eqid 
 |-  ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )
9 7 8 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 ) )
10 2 5 9 sylancl 
 |-  ( ( ph /\ R e. _V ) -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) )
11 10 ex 
 |-  ( ph -> ( R e. _V -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) ) )
12 iun0 
 |-  U_ n e. NN0 (/) = (/)
13 12 a1i 
 |-  ( -. R e. _V -> U_ n e. NN0 (/) = (/) )
14 reldmrelexp 
 |-  Rel dom ^r
15 14 ovprc1 
 |-  ( -. R e. _V -> ( R ^r n ) = (/) )
16 15 iuneq2d 
 |-  ( -. R e. _V -> U_ n e. NN0 ( R ^r n ) = U_ n e. NN0 (/) )
17 fvprc 
 |-  ( -. R e. _V -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = (/) )
18 13 16 17 3eqtr4rd 
 |-  ( -. R e. _V -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) )
19 11 18 pm2.61d1 
 |-  ( ph -> ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) )
20 breq 
 |-  ( ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) -> ( A ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) B <-> A U_ n e. NN0 ( R ^r n ) B ) )
21 eliun 
 |-  ( <. A , B >. e. U_ n e. NN0 ( R ^r n ) <-> E. n e. NN0 <. A , B >. e. ( R ^r n ) )
22 21 a1i 
 |-  ( ph -> ( <. A , B >. e. U_ n e. NN0 ( R ^r n ) <-> E. n e. NN0 <. A , B >. e. ( R ^r n ) ) )
23 df-br 
 |-  ( A U_ n e. NN0 ( R ^r n ) B <-> <. A , B >. e. U_ n e. NN0 ( R ^r n ) )
24 df-br 
 |-  ( A ( R ^r n ) B <-> <. A , B >. e. ( R ^r n ) )
25 24 rexbii 
 |-  ( E. n e. NN0 A ( R ^r n ) B <-> E. n e. NN0 <. A , B >. e. ( R ^r n ) )
26 22 23 25 3bitr4g 
 |-  ( ph -> ( A U_ n e. NN0 ( R ^r n ) B <-> E. n e. NN0 A ( R ^r n ) B ) )
27 20 26 sylan9bb 
 |-  ( ( ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) = U_ n e. NN0 ( R ^r n ) /\ ph ) -> ( A ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) )
28 19 27 mpancom 
 |-  ( ph -> ( A ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) )
29 df-rtrclrec 
 |-  t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )
30 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 ) )
31 30 breqd 
 |-  ( t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) -> ( A ( t*rec ` R ) B <-> A ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) B ) )
32 31 bibi1d 
 |-  ( t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) -> ( ( A ( t*rec ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) <-> ( A ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) ) )
33 32 imbi2d 
 |-  ( t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) -> ( ( ph -> ( A ( t*rec ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) ) <-> ( ph -> ( A ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) ) ) )
34 29 33 ax-mp 
 |-  ( ( ph -> ( A ( t*rec ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) ) <-> ( ph -> ( A ( ( r e. _V |-> U_ n e. NN0 ( r ^r n ) ) ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) ) )
35 28 34 mpbir 
 |-  ( ph -> ( A ( t*rec ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) )