Metamath Proof Explorer

Theorem rtrclexi

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

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

Proof

Step Hyp Ref Expression
1 rtrclexi.1 
 |-  A e. V
2 ssun1 
 |-  A C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
3 coundir 
 |-  ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) = ( ( A o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) u. ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
4 coundi 
 |-  ( A o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) = ( ( A o. A ) u. ( A o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
5 cossxp 
 |-  ( A o. A ) C_ ( dom A X. ran A )
6 ssun1 
 |-  dom A C_ ( dom A u. ran A )
7 ssun2 
 |-  ran A C_ ( dom A u. ran A )
8 xpss12 
 |-  ( ( dom A C_ ( dom A u. ran A ) /\ ran A C_ ( dom A u. ran A ) ) -> ( dom A X. ran A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
9 6 7 8 mp2an 
 |-  ( dom A X. ran A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
10 5 9 sstri 
 |-  ( A o. A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
11 cossxp 
 |-  ( A o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) X. ran A )
12 dmxpss 
 |-  dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) C_ ( dom A u. ran A )
13 xpss12 
 |-  ( ( dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) C_ ( dom A u. ran A ) /\ ran A C_ ( dom A u. ran A ) ) -> ( dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) X. ran A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
14 12 7 13 mp2an 
 |-  ( dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) X. ran A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
15 11 14 sstri 
 |-  ( A o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
16 10 15 unssi 
 |-  ( ( A o. A ) u. ( A o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
17 4 16 eqsstri 
 |-  ( A o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
18 coundi 
 |-  ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) = ( ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. A ) u. ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
19 cossxp 
 |-  ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. A ) C_ ( dom A X. ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
20 rnxpss 
 |-  ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) C_ ( dom A u. ran A )
21 xpss12 
 |-  ( ( dom A C_ ( dom A u. ran A ) /\ ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) C_ ( dom A u. ran A ) ) -> ( dom A X. ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
22 6 20 21 mp2an 
 |-  ( dom A X. ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
23 19 22 sstri 
 |-  ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. A ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
24 xpidtr 
 |-  ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
25 23 24 unssi 
 |-  ( ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. A ) u. ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
26 18 25 eqsstri 
 |-  ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
27 17 26 unssi 
 |-  ( ( A o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) u. ( ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
28 3 27 eqsstri 
 |-  ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
29 ssun2 
 |-  ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
30 28 29 sstri 
 |-  ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
31 dmun 
 |-  dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) = ( dom A u. dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
32 6 12 unssi 
 |-  ( dom A u. dom ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( dom A u. ran A )
33 31 32 eqsstri 
 |-  dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( dom A u. ran A )
34 rnun 
 |-  ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) = ( ran A u. ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
35 7 20 unssi 
 |-  ( ran A u. ran ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( dom A u. ran A )
36 34 35 eqsstri 
 |-  ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) C_ ( dom A u. ran A )
37 33 36 unssi 
 |-  ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( dom A u. ran A )
38 ssres2 
 |-  ( ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( dom A u. ran A ) -> ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( _I |` ( dom A u. ran A ) ) )
39 37 38 ax-mp 
 |-  ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( _I |` ( dom A u. ran A ) )
40 idssxp 
 |-  ( _I |` ( dom A u. ran A ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
41 39 40 sstri 
 |-  ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( ( dom A u. ran A ) X. ( dom A u. ran A ) )
42 41 29 sstri 
 |-  ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) )
43 id 
 |-  ( ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) -> ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
44 30 42 43 mp2an 
 |-  ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
45 1 elexi 
 |-  A e. _V
46 45 dmex 
 |-  dom A e. _V
47 45 rnex 
 |-  ran A e. _V
48 46 47 unex 
 |-  ( dom A u. ran A ) e. _V
49 48 48 xpex 
 |-  ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) e. _V
50 45 49 unex 
 |-  ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) e. _V
51 id 
 |-  ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
52 51 51 coeq12d 
 |-  ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( x o. x ) = ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
53 52 51 sseq12d 
 |-  ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( ( x o. x ) C_ x <-> ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
54 dmeq 
 |-  ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> dom x = dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
55 rneq 
 |-  ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ran x = ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) )
56 54 55 uneq12d 
 |-  ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( dom x u. ran x ) = ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
57 56 reseq2d 
 |-  ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( _I |` ( dom x u. ran x ) ) = ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) )
58 57 51 sseq12d 
 |-  ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( ( _I |` ( dom x u. ran x ) ) C_ x <-> ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) )
59 53 58 anbi12d 
 |-  ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) <-> ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) )
60 59 cleq2lem 
 |-  ( x = ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) -> ( ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) <-> ( A C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) ) )
61 50 60 spcev 
 |-  ( ( A C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) -> E. x ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) )
62 intexab 
 |-  ( E. x ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) <-> |^| { x | ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) } e. _V )
63 61 62 sylib 
 |-  ( ( A C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( ( ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) o. ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) /\ ( _I |` ( dom ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) u. ran ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) C_ ( A u. ( ( dom A u. ran A ) X. ( dom A u. ran A ) ) ) ) ) -> |^| { x | ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) } e. _V )
64 2 44 63 mp2an 
 |-  |^| { x | ( A C_ x /\ ( ( x o. x ) C_ x /\ ( _I |` ( dom x u. ran x ) ) C_ x ) ) } e. _V