Theorem ttcwf

Description: A set is well-founded iff its transitive closure is well-founded. As a corollary, the transitive closure of any well-founded set is a set. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcwf	|- ( A e. U. ( R1 " On ) <-> TC+ A e. U. ( R1 " On ) )

Proof

Step	Hyp	Ref	Expression
1		r1rankidb	|- ( A e. U. ( R1 " On ) -> A C_ ( R1 ` ( rank ` A ) ) )
2		r1tr	|- Tr ( R1 ` ( rank ` A ) )
3		ttcmin	|- ( ( A C_ ( R1 ` ( rank ` A ) ) /\ Tr ( R1 ` ( rank ` A ) ) ) -> TC+ A C_ ( R1 ` ( rank ` A ) ) )
4	1 2 3	sylancl	|- ( A e. U. ( R1 " On ) -> TC+ A C_ ( R1 ` ( rank ` A ) ) )
5		fvex	|- ( R1 ` ( rank ` A ) ) e. _V
6	5	elpw2	|- ( TC+ A e. ~P ( R1 ` ( rank ` A ) ) <-> TC+ A C_ ( R1 ` ( rank ` A ) ) )
7	4 6	sylibr	|- ( A e. U. ( R1 " On ) -> TC+ A e. ~P ( R1 ` ( rank ` A ) ) )
8		rankdmr1	|- ( rank ` A ) e. dom R1
9		r1sucg	|- ( ( rank ` A ) e. dom R1 -> ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) ) )
10	8 9	ax-mp	|- ( R1 ` suc ( rank ` A ) ) = ~P ( R1 ` ( rank ` A ) )
11	7 10	eleqtrrdi	|- ( A e. U. ( R1 " On ) -> TC+ A e. ( R1 ` suc ( rank ` A ) ) )
12		r1elwf	|- ( TC+ A e. ( R1 ` suc ( rank ` A ) ) -> TC+ A e. U. ( R1 " On ) )
13	11 12	syl	|- ( A e. U. ( R1 " On ) -> TC+ A e. U. ( R1 " On ) )
14		ttcid	|- A C_ TC+ A
15		sswf	|- ( ( TC+ A e. U. ( R1 " On ) /\ A C_ TC+ A ) -> A e. U. ( R1 " On ) )
16	14 15	mpan2	|- ( TC+ A e. U. ( R1 " On ) -> A e. U. ( R1 " On ) )
17	13 16	impbii	|- ( A e. U. ( R1 " On ) <-> TC+ A e. U. ( R1 " On ) )