Metamath Proof Explorer

Theorem dfrcl2

Description: Reflexive closure of a relation as union with restricted identity relation. (Contributed by RP, 6-Jun-2020)

Ref Expression
Assertion dfrcl2 
|- r* = ( x e. _V |-> ( ( _I |` ( dom x u. ran x ) ) u. x ) )

Proof

Step Hyp Ref Expression
1 df-rcl 
 |-  r* = ( x e. _V |-> |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } )
2 rabab 
 |-  { z e. _V | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } = { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) }
3 2 eqcomi 
 |-  { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } = { z e. _V | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) }
4 3 inteqi 
 |-  |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } = |^| { z e. _V | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) }
5 4 a1i 
 |-  ( x e. _V -> |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } = |^| { z e. _V | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } )
6 vex 
 |-  x e. _V
7 6 dmex 
 |-  dom x e. _V
8 6 rnex 
 |-  ran x e. _V
9 7 8 unex 
 |-  ( dom x u. ran x ) e. _V
10 resiexg 
 |-  ( ( dom x u. ran x ) e. _V -> ( _I |` ( dom x u. ran x ) ) e. _V )
11 9 10 ax-mp 
 |-  ( _I |` ( dom x u. ran x ) ) e. _V
12 11 6 unex 
 |-  ( ( _I |` ( dom x u. ran x ) ) u. x ) e. _V
13 12 a1i 
 |-  ( x e. _V -> ( ( _I |` ( dom x u. ran x ) ) u. x ) e. _V )
14 ssun2 
 |-  x C_ ( ( _I |` ( dom x u. ran x ) ) u. x )
15 dmun 
 |-  dom ( ( _I |` ( dom x u. ran x ) ) u. x ) = ( dom ( _I |` ( dom x u. ran x ) ) u. dom x )
16 dmresi 
 |-  dom ( _I |` ( dom x u. ran x ) ) = ( dom x u. ran x )
17 16 uneq1i 
 |-  ( dom ( _I |` ( dom x u. ran x ) ) u. dom x ) = ( ( dom x u. ran x ) u. dom x )
18 un23 
 |-  ( ( dom x u. ran x ) u. dom x ) = ( ( dom x u. dom x ) u. ran x )
19 unidm 
 |-  ( dom x u. dom x ) = dom x
20 19 uneq1i 
 |-  ( ( dom x u. dom x ) u. ran x ) = ( dom x u. ran x )
21 18 20 eqtri 
 |-  ( ( dom x u. ran x ) u. dom x ) = ( dom x u. ran x )
22 15 17 21 3eqtri 
 |-  dom ( ( _I |` ( dom x u. ran x ) ) u. x ) = ( dom x u. ran x )
23 rnun 
 |-  ran ( ( _I |` ( dom x u. ran x ) ) u. x ) = ( ran ( _I |` ( dom x u. ran x ) ) u. ran x )
24 rnresi 
 |-  ran ( _I |` ( dom x u. ran x ) ) = ( dom x u. ran x )
25 24 uneq1i 
 |-  ( ran ( _I |` ( dom x u. ran x ) ) u. ran x ) = ( ( dom x u. ran x ) u. ran x )
26 unass 
 |-  ( ( dom x u. ran x ) u. ran x ) = ( dom x u. ( ran x u. ran x ) )
27 unidm 
 |-  ( ran x u. ran x ) = ran x
28 27 uneq2i 
 |-  ( dom x u. ( ran x u. ran x ) ) = ( dom x u. ran x )
29 26 28 eqtri 
 |-  ( ( dom x u. ran x ) u. ran x ) = ( dom x u. ran x )
30 23 25 29 3eqtri 
 |-  ran ( ( _I |` ( dom x u. ran x ) ) u. x ) = ( dom x u. ran x )
31 22 30 uneq12i 
 |-  ( dom ( ( _I |` ( dom x u. ran x ) ) u. x ) u. ran ( ( _I |` ( dom x u. ran x ) ) u. x ) ) = ( ( dom x u. ran x ) u. ( dom x u. ran x ) )
32 unidm 
 |-  ( ( dom x u. ran x ) u. ( dom x u. ran x ) ) = ( dom x u. ran x )
33 31 32 eqtri 
 |-  ( dom ( ( _I |` ( dom x u. ran x ) ) u. x ) u. ran ( ( _I |` ( dom x u. ran x ) ) u. x ) ) = ( dom x u. ran x )
34 33 reseq2i 
 |-  ( _I |` ( dom ( ( _I |` ( dom x u. ran x ) ) u. x ) u. ran ( ( _I |` ( dom x u. ran x ) ) u. x ) ) ) = ( _I |` ( dom x u. ran x ) )
35 ssun1 
 |-  ( _I |` ( dom x u. ran x ) ) C_ ( ( _I |` ( dom x u. ran x ) ) u. x )
36 34 35 eqsstri 
 |-  ( _I |` ( dom ( ( _I |` ( dom x u. ran x ) ) u. x ) u. ran ( ( _I |` ( dom x u. ran x ) ) u. x ) ) ) C_ ( ( _I |` ( dom x u. ran x ) ) u. x )
37 14 36 pm3.2i 
 |-  ( x C_ ( ( _I |` ( dom x u. ran x ) ) u. x ) /\ ( _I |` ( dom ( ( _I |` ( dom x u. ran x ) ) u. x ) u. ran ( ( _I |` ( dom x u. ran x ) ) u. x ) ) ) C_ ( ( _I |` ( dom x u. ran x ) ) u. x ) )
38 dmeq 
 |-  ( z = ( ( _I |` ( dom x u. ran x ) ) u. x ) -> dom z = dom ( ( _I |` ( dom x u. ran x ) ) u. x ) )
39 rneq 
 |-  ( z = ( ( _I |` ( dom x u. ran x ) ) u. x ) -> ran z = ran ( ( _I |` ( dom x u. ran x ) ) u. x ) )
40 38 39 uneq12d 
 |-  ( z = ( ( _I |` ( dom x u. ran x ) ) u. x ) -> ( dom z u. ran z ) = ( dom ( ( _I |` ( dom x u. ran x ) ) u. x ) u. ran ( ( _I |` ( dom x u. ran x ) ) u. x ) ) )
41 40 reseq2d 
 |-  ( z = ( ( _I |` ( dom x u. ran x ) ) u. x ) -> ( _I |` ( dom z u. ran z ) ) = ( _I |` ( dom ( ( _I |` ( dom x u. ran x ) ) u. x ) u. ran ( ( _I |` ( dom x u. ran x ) ) u. x ) ) ) )
42 id 
 |-  ( z = ( ( _I |` ( dom x u. ran x ) ) u. x ) -> z = ( ( _I |` ( dom x u. ran x ) ) u. x ) )
43 41 42 sseq12d 
 |-  ( z = ( ( _I |` ( dom x u. ran x ) ) u. x ) -> ( ( _I |` ( dom z u. ran z ) ) C_ z <-> ( _I |` ( dom ( ( _I |` ( dom x u. ran x ) ) u. x ) u. ran ( ( _I |` ( dom x u. ran x ) ) u. x ) ) ) C_ ( ( _I |` ( dom x u. ran x ) ) u. x ) ) )
44 43 cleq2lem 
 |-  ( z = ( ( _I |` ( dom x u. ran x ) ) u. x ) -> ( ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) <-> ( x C_ ( ( _I |` ( dom x u. ran x ) ) u. x ) /\ ( _I |` ( dom ( ( _I |` ( dom x u. ran x ) ) u. x ) u. ran ( ( _I |` ( dom x u. ran x ) ) u. x ) ) ) C_ ( ( _I |` ( dom x u. ran x ) ) u. x ) ) ) )
45 44 intminss 
 |-  ( ( ( ( _I |` ( dom x u. ran x ) ) u. x ) e. _V /\ ( x C_ ( ( _I |` ( dom x u. ran x ) ) u. x ) /\ ( _I |` ( dom ( ( _I |` ( dom x u. ran x ) ) u. x ) u. ran ( ( _I |` ( dom x u. ran x ) ) u. x ) ) ) C_ ( ( _I |` ( dom x u. ran x ) ) u. x ) ) ) -> |^| { z e. _V | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } C_ ( ( _I |` ( dom x u. ran x ) ) u. x ) )
46 13 37 45 sylancl 
 |-  ( x e. _V -> |^| { z e. _V | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } C_ ( ( _I |` ( dom x u. ran x ) ) u. x ) )
47 5 46 eqsstrd 
 |-  ( x e. _V -> |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } C_ ( ( _I |` ( dom x u. ran x ) ) u. x ) )
48 dmss 
 |-  ( x C_ z -> dom x C_ dom z )
49 rnss 
 |-  ( x C_ z -> ran x C_ ran z )
50 unss12 
 |-  ( ( dom x C_ dom z /\ ran x C_ ran z ) -> ( dom x u. ran x ) C_ ( dom z u. ran z ) )
51 48 49 50 syl2anc 
 |-  ( x C_ z -> ( dom x u. ran x ) C_ ( dom z u. ran z ) )
52 dfss 
 |-  ( ( dom x u. ran x ) C_ ( dom z u. ran z ) <-> ( dom x u. ran x ) = ( ( dom x u. ran x ) i^i ( dom z u. ran z ) ) )
53 51 52 sylib 
 |-  ( x C_ z -> ( dom x u. ran x ) = ( ( dom x u. ran x ) i^i ( dom z u. ran z ) ) )
54 incom 
 |-  ( ( dom x u. ran x ) i^i ( dom z u. ran z ) ) = ( ( dom z u. ran z ) i^i ( dom x u. ran x ) )
55 53 54 eqtrdi 
 |-  ( x C_ z -> ( dom x u. ran x ) = ( ( dom z u. ran z ) i^i ( dom x u. ran x ) ) )
56 55 reseq2d 
 |-  ( x C_ z -> ( _I |` ( dom x u. ran x ) ) = ( _I |` ( ( dom z u. ran z ) i^i ( dom x u. ran x ) ) ) )
57 resres 
 |-  ( ( _I |` ( dom z u. ran z ) ) |` ( dom x u. ran x ) ) = ( _I |` ( ( dom z u. ran z ) i^i ( dom x u. ran x ) ) )
58 56 57 eqtr4di 
 |-  ( x C_ z -> ( _I |` ( dom x u. ran x ) ) = ( ( _I |` ( dom z u. ran z ) ) |` ( dom x u. ran x ) ) )
59 resss 
 |-  ( ( _I |` ( dom z u. ran z ) ) |` ( dom x u. ran x ) ) C_ ( _I |` ( dom z u. ran z ) )
60 59 a1i 
 |-  ( x C_ z -> ( ( _I |` ( dom z u. ran z ) ) |` ( dom x u. ran x ) ) C_ ( _I |` ( dom z u. ran z ) ) )
61 58 60 eqsstrd 
 |-  ( x C_ z -> ( _I |` ( dom x u. ran x ) ) C_ ( _I |` ( dom z u. ran z ) ) )
62 61 adantr 
 |-  ( ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) -> ( _I |` ( dom x u. ran x ) ) C_ ( _I |` ( dom z u. ran z ) ) )
63 simpr 
 |-  ( ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) -> ( _I |` ( dom z u. ran z ) ) C_ z )
64 62 63 sstrd 
 |-  ( ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) -> ( _I |` ( dom x u. ran x ) ) C_ z )
65 simpl 
 |-  ( ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) -> x C_ z )
66 64 65 unssd 
 |-  ( ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) -> ( ( _I |` ( dom x u. ran x ) ) u. x ) C_ z )
67 66 ax-gen 
 |-  A. z ( ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) -> ( ( _I |` ( dom x u. ran x ) ) u. x ) C_ z )
68 67 a1i 
 |-  ( x e. _V -> A. z ( ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) -> ( ( _I |` ( dom x u. ran x ) ) u. x ) C_ z ) )
69 ssintab 
 |-  ( ( ( _I |` ( dom x u. ran x ) ) u. x ) C_ |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } <-> A. z ( ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) -> ( ( _I |` ( dom x u. ran x ) ) u. x ) C_ z ) )
70 68 69 sylibr 
 |-  ( x e. _V -> ( ( _I |` ( dom x u. ran x ) ) u. x ) C_ |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } )
71 47 70 eqssd 
 |-  ( x e. _V -> |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } = ( ( _I |` ( dom x u. ran x ) ) u. x ) )
72 71 mpteq2ia 
 |-  ( x e. _V |-> |^| { z | ( x C_ z /\ ( _I |` ( dom z u. ran z ) ) C_ z ) } ) = ( x e. _V |-> ( ( _I |` ( dom x u. ran x ) ) u. x ) )
73 1 72 eqtri 
 |-  r* = ( x e. _V |-> ( ( _I |` ( dom x u. ran x ) ) u. x ) )