Theorem tcfr

Description: A set is well-founded if and only if its transitive closure is well-founded by e. . This characterization of well-founded sets is that in Definition I.9.20 of Kunen2 p. 53. (Contributed by Eric Schmidt, 26-Oct-2025)

	Ref	Expression
Hypothesis	tcfr.1	|- A e. _V
Assertion	tcfr	|- ( A e. U. ( R1 " On ) <-> _E Fr ( TC ` A ) )

Proof

Step	Hyp	Ref	Expression
1		tcfr.1	|- A e. _V
2		tcwf	|- ( A e. U. ( R1 " On ) -> ( TC ` A ) e. U. ( R1 " On ) )
3		r1elssi	|- ( ( TC ` A ) e. U. ( R1 " On ) -> ( TC ` A ) C_ U. ( R1 " On ) )
4		wffr	|- _E Fr U. ( R1 " On )
5		frss	|- ( ( TC ` A ) C_ U. ( R1 " On ) -> ( _E Fr U. ( R1 " On ) -> _E Fr ( TC ` A ) ) )
6	4 5	mpi	|- ( ( TC ` A ) C_ U. ( R1 " On ) -> _E Fr ( TC ` A ) )
7	2 3 6	3syl	|- ( A e. U. ( R1 " On ) -> _E Fr ( TC ` A ) )
8		tcid	|- ( A e. _V -> A C_ ( TC ` A ) )
9	1 8	ax-mp	|- A C_ ( TC ` A )
10		tctr	|- Tr ( TC ` A )
11		trfr	|- ( ( Tr ( TC ` A ) /\ _E Fr ( TC ` A ) ) -> ( TC ` A ) C_ U. ( R1 " On ) )
12	10 11	mpan	|- ( _E Fr ( TC ` A ) -> ( TC ` A ) C_ U. ( R1 " On ) )
13	9 12	sstrid	|- ( _E Fr ( TC ` A ) -> A C_ U. ( R1 " On ) )
14	1	r1elss	|- ( A e. U. ( R1 " On ) <-> A C_ U. ( R1 " On ) )
15	13 14	sylibr	|- ( _E Fr ( TC ` A ) -> A e. U. ( R1 " On ) )
16	7 15	impbii	|- ( A e. U. ( R1 " On ) <-> _E Fr ( TC ` A ) )