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	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		r1rankidb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
2		r1tr	⊢ Tr ( 𝑅1 ‘ ( rank ‘ 𝐴 ) )
3		ttcmin	⊢ ( ( 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∧ Tr ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) → TC+ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
4	1 2 3	sylancl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → TC+ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
5		fvex	⊢ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∈ V
6	5	elpw2	⊢ ( TC+ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ↔ TC+ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
7	4 6	sylibr	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → TC+ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
8		rankdmr1	⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1
9		r1sucg	⊢ ( ( rank ‘ 𝐴 ) ∈ dom 𝑅1 → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
10	8 9	ax-mp	⊢ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = 𝒫 ( 𝑅1 ‘ ( rank ‘ 𝐴 ) )
11	7 10	eleqtrrdi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → TC+ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )
12		r1elwf	⊢ ( TC+ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) → TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
13	11 12	syl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
14		ttcid	⊢ 𝐴 ⊆ TC+ 𝐴
15		sswf	⊢ ( ( TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ⊆ TC+ 𝐴 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
16	14 15	mpan2	⊢ ( TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
17	13 16	impbii	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )