Theorem unisucg

Description: A transitive class is equal to the union of its successor, closed form. Combines Theorem 4E of Enderton p. 72 and Exercise 6 of Enderton p. 73. (Contributed by NM, 30-Aug-1993) Generalize from unisuc . (Revised by BJ, 28-Dec-2024)

	Ref	Expression
Assertion	unisucg	$$⊢A\in V\to \left(\mathrm{Tr}A\leftrightarrow \bigcup \mathrm{suc}A=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ssequn1	$$⊢\bigcup A\subseteq A\leftrightarrow \bigcup A\cup A=A$$
2	1	a1i	$$⊢A\in V\to \left(\bigcup A\subseteq A\leftrightarrow \bigcup A\cup A=A\right)$$
3		df-tr	$$⊢\mathrm{Tr}A\leftrightarrow \bigcup A\subseteq A$$
4	3	a1i	$$⊢A\in V\to \left(\mathrm{Tr}A\leftrightarrow \bigcup A\subseteq A\right)$$
5		unisucs	$$⊢A\in V\to \bigcup \mathrm{suc}A=\bigcup A\cup A$$
6	5	eqeq1d	$$⊢A\in V\to \left(\bigcup \mathrm{suc}A=A\leftrightarrow \bigcup A\cup A=A\right)$$
7	2 4 6	3bitr4d	$$⊢A\in V\to \left(\mathrm{Tr}A\leftrightarrow \bigcup \mathrm{suc}A=A\right)$$