Metamath Proof Explorer


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 ( 𝐴𝑉 → ( Tr 𝐴 suc 𝐴 = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ssequn1 ( 𝐴𝐴 ↔ ( 𝐴𝐴 ) = 𝐴 )
2 1 a1i ( 𝐴𝑉 → ( 𝐴𝐴 ↔ ( 𝐴𝐴 ) = 𝐴 ) )
3 df-tr ( Tr 𝐴 𝐴𝐴 )
4 3 a1i ( 𝐴𝑉 → ( Tr 𝐴 𝐴𝐴 ) )
5 unisucs ( 𝐴𝑉 suc 𝐴 = ( 𝐴𝐴 ) )
6 5 eqeq1d ( 𝐴𝑉 → ( suc 𝐴 = 𝐴 ↔ ( 𝐴𝐴 ) = 𝐴 ) )
7 2 4 6 3bitr4d ( 𝐴𝑉 → ( Tr 𝐴 suc 𝐴 = 𝐴 ) )