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 e. V -> ( Tr A <-> U. suc A = A ) )

Proof

Step	Hyp	Ref	Expression
1		ssequn1	|- ( U. A C_ A <-> ( U. A u. A ) = A )
2	1	a1i	|- ( A e. V -> ( U. A C_ A <-> ( U. A u. A ) = A ) )
3		df-tr	|- ( Tr A <-> U. A C_ A )
4	3	a1i	|- ( A e. V -> ( Tr A <-> U. A C_ A ) )
5		unisucs	|- ( A e. V -> U. suc A = ( U. A u. A ) )
6	5	eqeq1d	|- ( A e. V -> ( U. suc A = A <-> ( U. A u. A ) = A ) )
7	2 4 6	3bitr4d	|- ( A e. V -> ( Tr A <-> U. suc A = A ) )