Metamath Proof Explorer

Theorem rclexi

Description: The reflexive closure of a set exists. (Contributed by RP, 27-Oct-2020)

Ref Expression
Hypothesis rclexi.1 
|- A e. V
Assertion rclexi 
|- |^| { x | ( A C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) } e. _V

Proof

Step Hyp Ref Expression
1 rclexi.1 
 |-  A e. V
2 ssun1 
 |-  A C_ ( A u. ( _I |` ( dom A u. ran A ) ) )
3 dmun 
 |-  dom ( A u. ( _I |` ( dom A u. ran A ) ) ) = ( dom A u. dom ( _I |` ( dom A u. ran A ) ) )
4 dmresi 
 |-  dom ( _I |` ( dom A u. ran A ) ) = ( dom A u. ran A )
5 4 uneq2i 
 |-  ( dom A u. dom ( _I |` ( dom A u. ran A ) ) ) = ( dom A u. ( dom A u. ran A ) )
6 ssun1 
 |-  dom A C_ ( dom A u. ran A )
7 ssequn1 
 |-  ( dom A C_ ( dom A u. ran A ) <-> ( dom A u. ( dom A u. ran A ) ) = ( dom A u. ran A ) )
8 6 7 mpbi 
 |-  ( dom A u. ( dom A u. ran A ) ) = ( dom A u. ran A )
9 3 5 8 3eqtri 
 |-  dom ( A u. ( _I |` ( dom A u. ran A ) ) ) = ( dom A u. ran A )
10 rnun 
 |-  ran ( A u. ( _I |` ( dom A u. ran A ) ) ) = ( ran A u. ran ( _I |` ( dom A u. ran A ) ) )
11 rnresi 
 |-  ran ( _I |` ( dom A u. ran A ) ) = ( dom A u. ran A )
12 11 uneq2i 
 |-  ( ran A u. ran ( _I |` ( dom A u. ran A ) ) ) = ( ran A u. ( dom A u. ran A ) )
13 ssun2 
 |-  ran A C_ ( dom A u. ran A )
14 ssequn1 
 |-  ( ran A C_ ( dom A u. ran A ) <-> ( ran A u. ( dom A u. ran A ) ) = ( dom A u. ran A ) )
15 13 14 mpbi 
 |-  ( ran A u. ( dom A u. ran A ) ) = ( dom A u. ran A )
16 10 12 15 3eqtri 
 |-  ran ( A u. ( _I |` ( dom A u. ran A ) ) ) = ( dom A u. ran A )
17 9 16 uneq12i 
 |-  ( dom ( A u. ( _I |` ( dom A u. ran A ) ) ) u. ran ( A u. ( _I |` ( dom A u. ran A ) ) ) ) = ( ( dom A u. ran A ) u. ( dom A u. ran A ) )
18 unidm 
 |-  ( ( dom A u. ran A ) u. ( dom A u. ran A ) ) = ( dom A u. ran A )
19 17 18 eqtri 
 |-  ( dom ( A u. ( _I |` ( dom A u. ran A ) ) ) u. ran ( A u. ( _I |` ( dom A u. ran A ) ) ) ) = ( dom A u. ran A )
20 19 reseq2i 
 |-  ( _I |` ( dom ( A u. ( _I |` ( dom A u. ran A ) ) ) u. ran ( A u. ( _I |` ( dom A u. ran A ) ) ) ) ) = ( _I |` ( dom A u. ran A ) )
21 ssun2 
 |-  ( _I |` ( dom A u. ran A ) ) C_ ( A u. ( _I |` ( dom A u. ran A ) ) )
22 20 21 eqsstri 
 |-  ( _I |` ( dom ( A u. ( _I |` ( dom A u. ran A ) ) ) u. ran ( A u. ( _I |` ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( _I |` ( dom A u. ran A ) ) )
23 1 elexi 
 |-  A e. _V
24 dmexg 
 |-  ( A e. V -> dom A e. _V )
25 rnexg 
 |-  ( A e. V -> ran A e. _V )
26 24 25 unexd 
 |-  ( A e. V -> ( dom A u. ran A ) e. _V )
27 26 resiexd 
 |-  ( A e. V -> ( _I |` ( dom A u. ran A ) ) e. _V )
28 1 27 ax-mp 
 |-  ( _I |` ( dom A u. ran A ) ) e. _V
29 23 28 unex 
 |-  ( A u. ( _I |` ( dom A u. ran A ) ) ) e. _V
30 dmeq 
 |-  ( x = ( A u. ( _I |` ( dom A u. ran A ) ) ) -> dom x = dom ( A u. ( _I |` ( dom A u. ran A ) ) ) )
31 rneq 
 |-  ( x = ( A u. ( _I |` ( dom A u. ran A ) ) ) -> ran x = ran ( A u. ( _I |` ( dom A u. ran A ) ) ) )
32 30 31 uneq12d 
 |-  ( x = ( A u. ( _I |` ( dom A u. ran A ) ) ) -> ( dom x u. ran x ) = ( dom ( A u. ( _I |` ( dom A u. ran A ) ) ) u. ran ( A u. ( _I |` ( dom A u. ran A ) ) ) ) )
33 32 reseq2d 
 |-  ( x = ( A u. ( _I |` ( dom A u. ran A ) ) ) -> ( _I |` ( dom x u. ran x ) ) = ( _I |` ( dom ( A u. ( _I |` ( dom A u. ran A ) ) ) u. ran ( A u. ( _I |` ( dom A u. ran A ) ) ) ) ) )
34 id 
 |-  ( x = ( A u. ( _I |` ( dom A u. ran A ) ) ) -> x = ( A u. ( _I |` ( dom A u. ran A ) ) ) )
35 33 34 sseq12d 
 |-  ( x = ( A u. ( _I |` ( dom A u. ran A ) ) ) -> ( ( _I |` ( dom x u. ran x ) ) C_ x <-> ( _I |` ( dom ( A u. ( _I |` ( dom A u. ran A ) ) ) u. ran ( A u. ( _I |` ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( _I |` ( dom A u. ran A ) ) ) ) )
36 35 cleq2lem 
 |-  ( x = ( A u. ( _I |` ( dom A u. ran A ) ) ) -> ( ( A C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) <-> ( A C_ ( A u. ( _I |` ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( _I |` ( dom A u. ran A ) ) ) u. ran ( A u. ( _I |` ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( _I |` ( dom A u. ran A ) ) ) ) ) )
37 29 36 spcev 
 |-  ( ( A C_ ( A u. ( _I |` ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( _I |` ( dom A u. ran A ) ) ) u. ran ( A u. ( _I |` ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( _I |` ( dom A u. ran A ) ) ) ) -> E. x ( A C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) )
38 intexab 
 |-  ( E. x ( A C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) <-> |^| { x | ( A C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) } e. _V )
39 37 38 sylib 
 |-  ( ( A C_ ( A u. ( _I |` ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( _I |` ( dom A u. ran A ) ) ) u. ran ( A u. ( _I |` ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( _I |` ( dom A u. ran A ) ) ) ) -> |^| { x | ( A C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) } e. _V )
40 2 22 39 mp2an 
 |-  |^| { x | ( A C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) } e. _V