Metamath Proof Explorer

Theorem tc2

Description: A variant of the definition of the transitive closure function, using instead the smallest transitive set containing A as a member, gives almost the same set, except that A itself must be added because it is not usually a member of ( TCA ) (and it is never a member if A is well-founded). (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Hypothesis tc2.1 
|- A e. _V
Assertion tc2 
|- ( ( TC ` A ) u. { A } ) = |^| { x | ( A e. x /\ Tr x ) }

Proof

Step Hyp Ref Expression
1 tc2.1 
 |-  A e. _V
2 tcvalg 
 |-  ( A e. _V -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } )
3 1 2 ax-mp 
 |-  ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) }
4 trss 
 |-  ( Tr x -> ( A e. x -> A C_ x ) )
5 4 imdistanri 
 |-  ( ( A e. x /\ Tr x ) -> ( A C_ x /\ Tr x ) )
6 5 ss2abi 
 |-  { x | ( A e. x /\ Tr x ) } C_ { x | ( A C_ x /\ Tr x ) }
7 intss 
 |-  ( { x | ( A e. x /\ Tr x ) } C_ { x | ( A C_ x /\ Tr x ) } -> |^| { x | ( A C_ x /\ Tr x ) } C_ |^| { x | ( A e. x /\ Tr x ) } )
8 6 7 ax-mp 
 |-  |^| { x | ( A C_ x /\ Tr x ) } C_ |^| { x | ( A e. x /\ Tr x ) }
9 3 8 eqsstri 
 |-  ( TC ` A ) C_ |^| { x | ( A e. x /\ Tr x ) }
10 1 elintab 
 |-  ( A e. |^| { x | ( A e. x /\ Tr x ) } <-> A. x ( ( A e. x /\ Tr x ) -> A e. x ) )
11 simpl 
 |-  ( ( A e. x /\ Tr x ) -> A e. x )
12 10 11 mpgbir 
 |-  A e. |^| { x | ( A e. x /\ Tr x ) }
13 1 snss 
 |-  ( A e. |^| { x | ( A e. x /\ Tr x ) } <-> { A } C_ |^| { x | ( A e. x /\ Tr x ) } )
14 12 13 mpbi 
 |-  { A } C_ |^| { x | ( A e. x /\ Tr x ) }
15 9 14 unssi 
 |-  ( ( TC ` A ) u. { A } ) C_ |^| { x | ( A e. x /\ Tr x ) }
16 1 snid 
 |-  A e. { A }
17 elun2 
 |-  ( A e. { A } -> A e. ( ( TC ` A ) u. { A } ) )
18 16 17 ax-mp 
 |-  A e. ( ( TC ` A ) u. { A } )
19 uniun 
 |-  U. ( ( TC ` A ) u. { A } ) = ( U. ( TC ` A ) u. U. { A } )
20 tctr 
 |-  Tr ( TC ` A )
21 df-tr 
 |-  ( Tr ( TC ` A ) <-> U. ( TC ` A ) C_ ( TC ` A ) )
22 20 21 mpbi 
 |-  U. ( TC ` A ) C_ ( TC ` A )
23 1 unisn 
 |-  U. { A } = A
24 tcid 
 |-  ( A e. _V -> A C_ ( TC ` A ) )
25 1 24 ax-mp 
 |-  A C_ ( TC ` A )
26 23 25 eqsstri 
 |-  U. { A } C_ ( TC ` A )
27 22 26 unssi 
 |-  ( U. ( TC ` A ) u. U. { A } ) C_ ( TC ` A )
28 19 27 eqsstri 
 |-  U. ( ( TC ` A ) u. { A } ) C_ ( TC ` A )
29 ssun1 
 |-  ( TC ` A ) C_ ( ( TC ` A ) u. { A } )
30 28 29 sstri 
 |-  U. ( ( TC ` A ) u. { A } ) C_ ( ( TC ` A ) u. { A } )
31 df-tr 
 |-  ( Tr ( ( TC ` A ) u. { A } ) <-> U. ( ( TC ` A ) u. { A } ) C_ ( ( TC ` A ) u. { A } ) )
32 30 31 mpbir 
 |-  Tr ( ( TC ` A ) u. { A } )
33 fvex 
 |-  ( TC ` A ) e. _V
34 snex 
 |-  { A } e. _V
35 33 34 unex 
 |-  ( ( TC ` A ) u. { A } ) e. _V
36 eleq2 
 |-  ( x = ( ( TC ` A ) u. { A } ) -> ( A e. x <-> A e. ( ( TC ` A ) u. { A } ) ) )
37 treq 
 |-  ( x = ( ( TC ` A ) u. { A } ) -> ( Tr x <-> Tr ( ( TC ` A ) u. { A } ) ) )
38 36 37 anbi12d 
 |-  ( x = ( ( TC ` A ) u. { A } ) -> ( ( A e. x /\ Tr x ) <-> ( A e. ( ( TC ` A ) u. { A } ) /\ Tr ( ( TC ` A ) u. { A } ) ) ) )
39 35 38 elab 
 |-  ( ( ( TC ` A ) u. { A } ) e. { x | ( A e. x /\ Tr x ) } <-> ( A e. ( ( TC ` A ) u. { A } ) /\ Tr ( ( TC ` A ) u. { A } ) ) )
40 18 32 39 mpbir2an 
 |-  ( ( TC ` A ) u. { A } ) e. { x | ( A e. x /\ Tr x ) }
41 intss1 
 |-  ( ( ( TC ` A ) u. { A } ) e. { x | ( A e. x /\ Tr x ) } -> |^| { x | ( A e. x /\ Tr x ) } C_ ( ( TC ` A ) u. { A } ) )
42 40 41 ax-mp 
 |-  |^| { x | ( A e. x /\ Tr x ) } C_ ( ( TC ` A ) u. { A } )
43 15 42 eqssi 
 |-  ( ( TC ` A ) u. { A } ) = |^| { x | ( A e. x /\ Tr x ) }