Metamath Proof Explorer

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 \in V$
	Assertion	tcfr	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow E Fr TC (A)$

Proof

Step	Hyp	Ref	Expression
1		tcfr.1	$⊢ A \in V$
2		tcwf	$⊢ A \in ⋃ R_{1} [On] \to TC (A) \in ⋃ R_{1} [On]$
3		r1elssi	$⊢ TC (A) \in ⋃ R_{1} [On] \to TC (A) \subseteq ⋃ R_{1} [On]$
4		wffr	$⊢ E Fr ⋃ R_{1} [On]$
5		frss	$⊢ TC (A) \subseteq ⋃ R_{1} [On] \to (E Fr ⋃ R_{1} [On] \to E Fr TC (A))$
6	4 5	mpi	$⊢ TC (A) \subseteq ⋃ R_{1} [On] \to E Fr TC (A)$
7	2 3 6	3syl	$⊢ A \in ⋃ R_{1} [On] \to E Fr TC (A)$
8		tcid	$⊢ A \in V \to A \subseteq TC (A)$
9	1 8	ax-mp	$⊢ A \subseteq TC (A)$
10		tctr	$⊢ Tr TC (A)$
11		trfr	$⊢ (Tr TC (A) \land E Fr TC (A)) \to TC (A) \subseteq ⋃ R_{1} [On]$
12	10 11	mpan	$⊢ E Fr TC (A) \to TC (A) \subseteq ⋃ R_{1} [On]$
13	9 12	sstrid	$⊢ E Fr TC (A) \to A \subseteq ⋃ R_{1} [On]$
14	1	r1elss	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow A \subseteq ⋃ R_{1} [On]$
15	13 14	sylibr	$⊢ E Fr TC (A) \to A \in ⋃ R_{1} [On]$
16	7 15	impbii	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow E Fr TC (A)$