Metamath Proof Explorer

Theorem corclrcl

Description: The reflexive closure is idempotent. (Contributed by RP, 13-Jun-2020)

Ref Expression
Assertion corclrcl 
|- ( r* o. r* ) = r*

Proof

Step Hyp Ref Expression
1 dfrcl4 
 |-  r* = ( a e. _V |-> U_ i e. { 0 , 1 } ( a ^r i ) )
2 dfrcl4 
 |-  r* = ( b e. _V |-> U_ j e. { 0 , 1 } ( b ^r j ) )
3 dfrcl4 
 |-  r* = ( c e. _V |-> U_ k e. { 0 , 1 } ( c ^r k ) )
4 prex 
 |-  { 0 , 1 } e. _V
5 unidm 
 |-  ( { 0 , 1 } u. { 0 , 1 } ) = { 0 , 1 }
6 5 eqcomi 
 |-  { 0 , 1 } = ( { 0 , 1 } u. { 0 , 1 } )
7 oveq2 
 |-  ( k = j -> ( d ^r k ) = ( d ^r j ) )
8 7 cbviunv 
 |-  U_ k e. { 0 , 1 } ( d ^r k ) = U_ j e. { 0 , 1 } ( d ^r j )
9 1ex 
 |-  1 e. _V
10 oveq2 
 |-  ( i = 1 -> ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = ( U_ j e. { 0 , 1 } ( d ^r j ) ^r 1 ) )
11 9 10 iunxsn 
 |-  U_ i e. { 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = ( U_ j e. { 0 , 1 } ( d ^r j ) ^r 1 )
12 ovex 
 |-  ( d ^r j ) e. _V
13 4 12 iunex 
 |-  U_ j e. { 0 , 1 } ( d ^r j ) e. _V
14 relexp1g 
 |-  ( U_ j e. { 0 , 1 } ( d ^r j ) e. _V -> ( U_ j e. { 0 , 1 } ( d ^r j ) ^r 1 ) = U_ j e. { 0 , 1 } ( d ^r j ) )
15 13 14 ax-mp 
 |-  ( U_ j e. { 0 , 1 } ( d ^r j ) ^r 1 ) = U_ j e. { 0 , 1 } ( d ^r j )
16 11 15 eqtri 
 |-  U_ i e. { 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = U_ j e. { 0 , 1 } ( d ^r j )
17 16 eqcomi 
 |-  U_ j e. { 0 , 1 } ( d ^r j ) = U_ i e. { 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i )
18 8 17 eqtri 
 |-  U_ k e. { 0 , 1 } ( d ^r k ) = U_ i e. { 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i )
19 snsspr2 
 |-  { 1 } C_ { 0 , 1 }
20 iunss1 
 |-  ( { 1 } C_ { 0 , 1 } -> U_ i e. { 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) C_ U_ i e. { 0 , 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) )
21 19 20 ax-mp 
 |-  U_ i e. { 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) C_ U_ i e. { 0 , 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i )
22 18 21 eqsstri 
 |-  U_ k e. { 0 , 1 } ( d ^r k ) C_ U_ i e. { 0 , 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i )
23 c0ex 
 |-  0 e. _V
24 23 prid1 
 |-  0 e. { 0 , 1 }
25 oveq2 
 |-  ( k = 0 -> ( d ^r k ) = ( d ^r 0 ) )
26 25 ssiun2s 
 |-  ( 0 e. { 0 , 1 } -> ( d ^r 0 ) C_ U_ k e. { 0 , 1 } ( d ^r k ) )
27 24 26 ax-mp 
 |-  ( d ^r 0 ) C_ U_ k e. { 0 , 1 } ( d ^r k )
28 oveq2 
 |-  ( j = k -> ( d ^r j ) = ( d ^r k ) )
29 28 cbviunv 
 |-  U_ j e. { 0 , 1 } ( d ^r j ) = U_ k e. { 0 , 1 } ( d ^r k )
30 29 eqimssi 
 |-  U_ j e. { 0 , 1 } ( d ^r j ) C_ U_ k e. { 0 , 1 } ( d ^r k )
31 unss12 
 |-  ( ( ( d ^r 0 ) C_ U_ k e. { 0 , 1 } ( d ^r k ) /\ U_ j e. { 0 , 1 } ( d ^r j ) C_ U_ k e. { 0 , 1 } ( d ^r k ) ) -> ( ( d ^r 0 ) u. U_ j e. { 0 , 1 } ( d ^r j ) ) C_ ( U_ k e. { 0 , 1 } ( d ^r k ) u. U_ k e. { 0 , 1 } ( d ^r k ) ) )
32 27 30 31 mp2an 
 |-  ( ( d ^r 0 ) u. U_ j e. { 0 , 1 } ( d ^r j ) ) C_ ( U_ k e. { 0 , 1 } ( d ^r k ) u. U_ k e. { 0 , 1 } ( d ^r k ) )
33 df-pr 
 |-  { 0 , 1 } = ( { 0 } u. { 1 } )
34 iuneq1 
 |-  ( { 0 , 1 } = ( { 0 } u. { 1 } ) -> U_ i e. { 0 , 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = U_ i e. ( { 0 } u. { 1 } ) ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) )
35 33 34 ax-mp 
 |-  U_ i e. { 0 , 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = U_ i e. ( { 0 } u. { 1 } ) ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i )
36 iunxun 
 |-  U_ i e. ( { 0 } u. { 1 } ) ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = ( U_ i e. { 0 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) u. U_ i e. { 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) )
37 oveq2 
 |-  ( i = 0 -> ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = ( U_ j e. { 0 , 1 } ( d ^r j ) ^r 0 ) )
38 23 37 iunxsn 
 |-  U_ i e. { 0 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = ( U_ j e. { 0 , 1 } ( d ^r j ) ^r 0 )
39 vex 
 |-  d e. _V
40 0nn0 
 |-  0 e. NN0
41 1nn0 
 |-  1 e. NN0
42 prssi 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) -> { 0 , 1 } C_ NN0 )
43 40 41 42 mp2an 
 |-  { 0 , 1 } C_ NN0
44 24 24 elini 
 |-  0 e. ( { 0 , 1 } i^i { 0 , 1 } )
45 44 ne0ii 
 |-  ( { 0 , 1 } i^i { 0 , 1 } ) =/= (/)
46 iunrelexp0 
 |-  ( ( d e. _V /\ { 0 , 1 } C_ NN0 /\ ( { 0 , 1 } i^i { 0 , 1 } ) =/= (/) ) -> ( U_ j e. { 0 , 1 } ( d ^r j ) ^r 0 ) = ( d ^r 0 ) )
47 39 43 45 46 mp3an 
 |-  ( U_ j e. { 0 , 1 } ( d ^r j ) ^r 0 ) = ( d ^r 0 )
48 38 47 eqtri 
 |-  U_ i e. { 0 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = ( d ^r 0 )
49 48 16 uneq12i 
 |-  ( U_ i e. { 0 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) u. U_ i e. { 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) ) = ( ( d ^r 0 ) u. U_ j e. { 0 , 1 } ( d ^r j ) )
50 36 49 eqtri 
 |-  U_ i e. ( { 0 } u. { 1 } ) ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = ( ( d ^r 0 ) u. U_ j e. { 0 , 1 } ( d ^r j ) )
51 35 50 eqtri 
 |-  U_ i e. { 0 , 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) = ( ( d ^r 0 ) u. U_ j e. { 0 , 1 } ( d ^r j ) )
52 iunxun 
 |-  U_ k e. ( { 0 , 1 } u. { 0 , 1 } ) ( d ^r k ) = ( U_ k e. { 0 , 1 } ( d ^r k ) u. U_ k e. { 0 , 1 } ( d ^r k ) )
53 32 51 52 3sstr4i 
 |-  U_ i e. { 0 , 1 } ( U_ j e. { 0 , 1 } ( d ^r j ) ^r i ) C_ U_ k e. ( { 0 , 1 } u. { 0 , 1 } ) ( d ^r k )
54 1 2 3 4 4 6 22 22 53 comptiunov2i 
 |-  ( r* o. r* ) = r*