Theorem ttcwf3

Description: The sets whose transitive closures are sets are precisely the well-founded sets, assuming Regularity. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcwf3	⊢ ( TC+ 𝐴 ∈ V ↔ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )

Proof

Step	Hyp	Ref	Expression
1		ttcwf2	⊢ ( TC+ 𝐴 ∈ V ↔ TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
2		ttcwf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ TC+ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
3	1 2	bitr4i	⊢ ( TC+ 𝐴 ∈ V ↔ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )