Metamath Proof Explorer

Theorem trclexi

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

Ref Expression
Hypothesis trclexi.1 
|- A e. V
Assertion trclexi 
|- |^| { x | ( A C_ x /\ ( x o. x ) C_ x ) } e. _V

Proof

Step Hyp Ref Expression
1 trclexi.1 
 |-  A e. V
2 ssun1 
 |-  A C_ ( A u. ( dom A X. ran A ) )
3 coundir 
 |-  ( ( A u. ( dom A X. ran A ) ) o. ( A u. ( dom A X. ran A ) ) ) = ( ( A o. ( A u. ( dom A X. ran A ) ) ) u. ( ( dom A X. ran A ) o. ( A u. ( dom A X. ran A ) ) ) )
4 coundi 
 |-  ( A o. ( A u. ( dom A X. ran A ) ) ) = ( ( A o. A ) u. ( A o. ( dom A X. ran A ) ) )
5 cossxp 
 |-  ( A o. A ) C_ ( dom A X. ran A )
6 cossxp 
 |-  ( A o. ( dom A X. ran A ) ) C_ ( dom ( dom A X. ran A ) X. ran A )
7 dmxpss 
 |-  dom ( dom A X. ran A ) C_ dom A
8 xpss1 
 |-  ( dom ( dom A X. ran A ) C_ dom A -> ( dom ( dom A X. ran A ) X. ran A ) C_ ( dom A X. ran A ) )
9 7 8 ax-mp 
 |-  ( dom ( dom A X. ran A ) X. ran A ) C_ ( dom A X. ran A )
10 6 9 sstri 
 |-  ( A o. ( dom A X. ran A ) ) C_ ( dom A X. ran A )
11 5 10 unssi 
 |-  ( ( A o. A ) u. ( A o. ( dom A X. ran A ) ) ) C_ ( dom A X. ran A )
12 4 11 eqsstri 
 |-  ( A o. ( A u. ( dom A X. ran A ) ) ) C_ ( dom A X. ran A )
13 coundi 
 |-  ( ( dom A X. ran A ) o. ( A u. ( dom A X. ran A ) ) ) = ( ( ( dom A X. ran A ) o. A ) u. ( ( dom A X. ran A ) o. ( dom A X. ran A ) ) )
14 cossxp 
 |-  ( ( dom A X. ran A ) o. A ) C_ ( dom A X. ran ( dom A X. ran A ) )
15 rnxpss 
 |-  ran ( dom A X. ran A ) C_ ran A
16 xpss2 
 |-  ( ran ( dom A X. ran A ) C_ ran A -> ( dom A X. ran ( dom A X. ran A ) ) C_ ( dom A X. ran A ) )
17 15 16 ax-mp 
 |-  ( dom A X. ran ( dom A X. ran A ) ) C_ ( dom A X. ran A )
18 14 17 sstri 
 |-  ( ( dom A X. ran A ) o. A ) C_ ( dom A X. ran A )
19 xptrrel 
 |-  ( ( dom A X. ran A ) o. ( dom A X. ran A ) ) C_ ( dom A X. ran A )
20 18 19 unssi 
 |-  ( ( ( dom A X. ran A ) o. A ) u. ( ( dom A X. ran A ) o. ( dom A X. ran A ) ) ) C_ ( dom A X. ran A )
21 13 20 eqsstri 
 |-  ( ( dom A X. ran A ) o. ( A u. ( dom A X. ran A ) ) ) C_ ( dom A X. ran A )
22 12 21 unssi 
 |-  ( ( A o. ( A u. ( dom A X. ran A ) ) ) u. ( ( dom A X. ran A ) o. ( A u. ( dom A X. ran A ) ) ) ) C_ ( dom A X. ran A )
23 3 22 eqsstri 
 |-  ( ( A u. ( dom A X. ran A ) ) o. ( A u. ( dom A X. ran A ) ) ) C_ ( dom A X. ran A )
24 ssun2 
 |-  ( dom A X. ran A ) C_ ( A u. ( dom A X. ran A ) )
25 23 24 sstri 
 |-  ( ( A u. ( dom A X. ran A ) ) o. ( A u. ( dom A X. ran A ) ) ) C_ ( A u. ( dom A X. ran A ) )
26 1 elexi 
 |-  A e. _V
27 26 dmex 
 |-  dom A e. _V
28 26 rnex 
 |-  ran A e. _V
29 27 28 xpex 
 |-  ( dom A X. ran A ) e. _V
30 26 29 unex 
 |-  ( A u. ( dom A X. ran A ) ) e. _V
31 trcleq2lem 
 |-  ( x = ( A u. ( dom A X. ran A ) ) -> ( ( A C_ x /\ ( x o. x ) C_ x ) <-> ( A C_ ( A u. ( dom A X. ran A ) ) /\ ( ( A u. ( dom A X. ran A ) ) o. ( A u. ( dom A X. ran A ) ) ) C_ ( A u. ( dom A X. ran A ) ) ) ) )
32 30 31 spcev 
 |-  ( ( A C_ ( A u. ( dom A X. ran A ) ) /\ ( ( A u. ( dom A X. ran A ) ) o. ( A u. ( dom A X. ran A ) ) ) C_ ( A u. ( dom A X. ran A ) ) ) -> E. x ( A C_ x /\ ( x o. x ) C_ x ) )
33 intexab 
 |-  ( E. x ( A C_ x /\ ( x o. x ) C_ x ) <-> |^| { x | ( A C_ x /\ ( x o. x ) C_ x ) } e. _V )
34 32 33 sylib 
 |-  ( ( A C_ ( A u. ( dom A X. ran A ) ) /\ ( ( A u. ( dom A X. ran A ) ) o. ( A u. ( dom A X. ran A ) ) ) C_ ( A u. ( dom A X. ran A ) ) ) -> |^| { x | ( A C_ x /\ ( x o. x ) C_ x ) } e. _V )
35 2 25 34 mp2an 
 |-  |^| { x | ( A C_ x /\ ( x o. x ) C_ x ) } e. _V