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	⊢ 𝐴 ∈ V
Assertion	tcfr	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ E Fr ( TC ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		tcfr.1	⊢ 𝐴 ∈ V
2		tcwf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( TC ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) )
3		r1elssi	⊢ ( ( TC ‘ 𝐴 ) ∈ ∪ ( 𝑅1 “ On ) → ( TC ‘ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) )
4		wffr	⊢ E Fr ∪ ( 𝑅1 “ On )
5		frss	⊢ ( ( TC ‘ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) → ( E Fr ∪ ( 𝑅1 “ On ) → E Fr ( TC ‘ 𝐴 ) ) )
6	4 5	mpi	⊢ ( ( TC ‘ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) → E Fr ( TC ‘ 𝐴 ) )
7	2 3 6	3syl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → E Fr ( TC ‘ 𝐴 ) )
8		tcid	⊢ ( 𝐴 ∈ V → 𝐴 ⊆ ( TC ‘ 𝐴 ) )
9	1 8	ax-mp	⊢ 𝐴 ⊆ ( TC ‘ 𝐴 )
10		tctr	⊢ Tr ( TC ‘ 𝐴 )
11		trfr	⊢ ( ( Tr ( TC ‘ 𝐴 ) ∧ E Fr ( TC ‘ 𝐴 ) ) → ( TC ‘ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) )
12	10 11	mpan	⊢ ( E Fr ( TC ‘ 𝐴 ) → ( TC ‘ 𝐴 ) ⊆ ∪ ( 𝑅1 “ On ) )
13	9 12	sstrid	⊢ ( E Fr ( TC ‘ 𝐴 ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
14	1	r1elss	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
15	13 14	sylibr	⊢ ( E Fr ( TC ‘ 𝐴 ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
16	7 15	impbii	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ E Fr ( TC ‘ 𝐴 ) )