Metamath Proof Explorer

Theorem tcwf

Description: The transitive closure function is well-founded if its argument is. (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Assertion tcwf 
|- ( A e. U. ( R1 " On ) -> ( TC ` A ) e. U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 r1elssi 
 |-  ( A e. U. ( R1 " On ) -> A C_ U. ( R1 " On ) )
2 dftr3 
 |-  ( Tr U. ( R1 " On ) <-> A. x e. U. ( R1 " On ) x C_ U. ( R1 " On ) )
3 r1elssi 
 |-  ( x e. U. ( R1 " On ) -> x C_ U. ( R1 " On ) )
4 2 3 mprgbir 
 |-  Tr U. ( R1 " On )
5 tcmin 
 |-  ( A e. U. ( R1 " On ) -> ( ( A C_ U. ( R1 " On ) /\ Tr U. ( R1 " On ) ) -> ( TC ` A ) C_ U. ( R1 " On ) ) )
6 4 5 mpan2i 
 |-  ( A e. U. ( R1 " On ) -> ( A C_ U. ( R1 " On ) -> ( TC ` A ) C_ U. ( R1 " On ) ) )
7 1 6 mpd 
 |-  ( A e. U. ( R1 " On ) -> ( TC ` A ) C_ U. ( R1 " On ) )
8 fvex 
 |-  ( TC ` A ) e. _V
9 8 r1elss 
 |-  ( ( TC ` A ) e. U. ( R1 " On ) <-> ( TC ` A ) C_ U. ( R1 " On ) )
10 7 9 sylibr 
 |-  ( A e. U. ( R1 " On ) -> ( TC ` A ) e. U. ( R1 " On ) )