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	Could not format assertion : No typesetting found for |- ( A e. U. ( R1 " On ) <-> TC+ A e. U. ( R1 " On ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		r1rankidb	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to A\subseteq R_1\left(\mathrm{rank}\left(A\right)\right)$$
2		r1tr	$$⊢\mathrm{Tr}{R}_1\left(\mathrm{rank}\left(A\right)\right)$$
3		ttcmin	Could not format ( ( A C_ ( R1 ` ( rank ` A ) ) /\ Tr ( R1 ` ( rank ` A ) ) ) -> TC+ A C_ ( R1 ` ( rank ` A ) ) ) : No typesetting found for |- ( ( A C_ ( R1 ` ( rank ` A ) ) /\ Tr ( R1 ` ( rank ` A ) ) ) -> TC+ A C_ ( R1 ` ( rank ` A ) ) ) with typecode |-
4	1 2 3	sylancl	Could not format ( A e. U. ( R1 " On ) -> TC+ A C_ ( R1 ` ( rank ` A ) ) ) : No typesetting found for |- ( A e. U. ( R1 " On ) -> TC+ A C_ ( R1 ` ( rank ` A ) ) ) with typecode |-
5		fvex	$$⊢R_1\left(\mathrm{rank}\left(A\right)\right)\in \mathrm{V}$$
6	5	elpw2	Could not format ( TC+ A e. ~P ( R1 ` ( rank ` A ) ) <-> TC+ A C_ ( R1 ` ( rank ` A ) ) ) : No typesetting found for |- ( TC+ A e. ~P ( R1 ` ( rank ` A ) ) <-> TC+ A C_ ( R1 ` ( rank ` A ) ) ) with typecode |-
7	4 6	sylibr	Could not format ( A e. U. ( R1 " On ) -> TC+ A e. ~P ( R1 ` ( rank ` A ) ) ) : No typesetting found for |- ( A e. U. ( R1 " On ) -> TC+ A e. ~P ( R1 ` ( rank ` A ) ) ) with typecode |-
8		rankdmr1	$$⊢\mathrm{rank}\left(A\right)\in \mathrm{dom}{R}_1$$
9		r1sucg	$$⊢\mathrm{rank}\left(A\right)\in \mathrm{dom}{R}_1\to R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)=𝒫R_1\left(\mathrm{rank}\left(A\right)\right)$$
10	8 9	ax-mp	$$⊢R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)=𝒫R_1\left(\mathrm{rank}\left(A\right)\right)$$
11	7 10	eleqtrrdi	Could not format ( A e. U. ( R1 " On ) -> TC+ A e. ( R1 ` suc ( rank ` A ) ) ) : No typesetting found for |- ( A e. U. ( R1 " On ) -> TC+ A e. ( R1 ` suc ( rank ` A ) ) ) with typecode |-
12		r1elwf	Could not format ( TC+ A e. ( R1 ` suc ( rank ` A ) ) -> TC+ A e. U. ( R1 " On ) ) : No typesetting found for |- ( TC+ A e. ( R1 ` suc ( rank ` A ) ) -> TC+ A e. U. ( R1 " On ) ) with typecode |-
13	11 12	syl	Could not format ( A e. U. ( R1 " On ) -> TC+ A e. U. ( R1 " On ) ) : No typesetting found for |- ( A e. U. ( R1 " On ) -> TC+ A e. U. ( R1 " On ) ) with typecode |-
14		ttcid	Could not format A C_ TC+ A : No typesetting found for |- A C_ TC+ A with typecode |-
15		sswf	Could not format ( ( TC+ A e. U. ( R1 " On ) /\ A C_ TC+ A ) -> A e. U. ( R1 " On ) ) : No typesetting found for |- ( ( TC+ A e. U. ( R1 " On ) /\ A C_ TC+ A ) -> A e. U. ( R1 " On ) ) with typecode |-
16	14 15	mpan2	Could not format ( TC+ A e. U. ( R1 " On ) -> A e. U. ( R1 " On ) ) : No typesetting found for |- ( TC+ A e. U. ( R1 " On ) -> A e. U. ( R1 " On ) ) with typecode |-
17	13 16	impbii	Could not format ( A e. U. ( R1 " On ) <-> TC+ A e. U. ( R1 " On ) ) : No typesetting found for |- ( A e. U. ( R1 " On ) <-> TC+ A e. U. ( R1 " On ) ) with typecode |-