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 𝐴 = 𝐴 ) ) |
| 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 𝐴 = 𝐴 ) ) |