Metamath Proof Explorer

Theorem relexp0g

Description: A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020)

Ref Expression
Assertion relexp0g 
|- ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( R e. V -> ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) )
2 simprr 
 |-  ( ( R e. V /\ ( r = R /\ n = 0 ) ) -> n = 0 )
3 2 iftrued 
 |-  ( ( R e. V /\ ( r = R /\ n = 0 ) ) -> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) = ( _I |` ( dom r u. ran r ) ) )
4 dmeq 
 |-  ( r = R -> dom r = dom R )
5 rneq 
 |-  ( r = R -> ran r = ran R )
6 4 5 uneq12d 
 |-  ( r = R -> ( dom r u. ran r ) = ( dom R u. ran R ) )
7 6 reseq2d 
 |-  ( r = R -> ( _I |` ( dom r u. ran r ) ) = ( _I |` ( dom R u. ran R ) ) )
8 7 ad2antrl 
 |-  ( ( R e. V /\ ( r = R /\ n = 0 ) ) -> ( _I |` ( dom r u. ran r ) ) = ( _I |` ( dom R u. ran R ) ) )
9 3 8 eqtrd 
 |-  ( ( R e. V /\ ( r = R /\ n = 0 ) ) -> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) = ( _I |` ( dom R u. ran R ) ) )
10 elex 
 |-  ( R e. V -> R e. _V )
11 0nn0 
 |-  0 e. NN0
12 11 a1i 
 |-  ( R e. V -> 0 e. NN0 )
13 dmexg 
 |-  ( R e. V -> dom R e. _V )
14 rnexg 
 |-  ( R e. V -> ran R e. _V )
15 unexg 
 |-  ( ( dom R e. _V /\ ran R e. _V ) -> ( dom R u. ran R ) e. _V )
16 13 14 15 syl2anc 
 |-  ( R e. V -> ( dom R u. ran R ) e. _V )
17 resiexg 
 |-  ( ( dom R u. ran R ) e. _V -> ( _I |` ( dom R u. ran R ) ) e. _V )
18 16 17 syl 
 |-  ( R e. V -> ( _I |` ( dom R u. ran R ) ) e. _V )
19 1 9 10 12 18 ovmpod 
 |-  ( R e. V -> ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) 0 ) = ( _I |` ( dom R u. ran R ) ) )
20 df-relexp 
 |-  ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) )
21 oveq 
 |-  ( ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) -> ( R ^r 0 ) = ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) 0 ) )
22 21 eqeq1d 
 |-  ( ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) -> ( ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) <-> ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) 0 ) = ( _I |` ( dom R u. ran R ) ) ) )
23 22 imbi2d 
 |-  ( ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) -> ( ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) ) <-> ( R e. V -> ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) 0 ) = ( _I |` ( dom R u. ran R ) ) ) ) )
24 20 23 ax-mp 
 |-  ( ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) ) <-> ( R e. V -> ( R ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) ) 0 ) = ( _I |` ( dom R u. ran R ) ) ) )
25 19 24 mpbir 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )