Description: A transitive class is equal to the union of its successor. Combines Theorem 4E of Enderton p. 72 and Exercise 6 of Enderton p. 73. (Contributed by NM, 30-Aug-1993)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | unisuc.1 | ⊢ 𝐴 ∈ V | |
| Assertion | unisuc | ⊢ ( Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | unisuc.1 | ⊢ 𝐴 ∈ V | |
| 2 | ssequn1 | ⊢ ( ∪ 𝐴 ⊆ 𝐴 ↔ ( ∪ 𝐴 ∪ 𝐴 ) = 𝐴 ) | |
| 3 | df-tr | ⊢ ( Tr 𝐴 ↔ ∪ 𝐴 ⊆ 𝐴 ) | |
| 4 | df-suc | ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } ) | |
| 5 | 4 | unieqi | ⊢ ∪ suc 𝐴 = ∪ ( 𝐴 ∪ { 𝐴 } ) |
| 6 | uniun | ⊢ ∪ ( 𝐴 ∪ { 𝐴 } ) = ( ∪ 𝐴 ∪ ∪ { 𝐴 } ) | |
| 7 | 1 | unisn | ⊢ ∪ { 𝐴 } = 𝐴 |
| 8 | 7 | uneq2i | ⊢ ( ∪ 𝐴 ∪ ∪ { 𝐴 } ) = ( ∪ 𝐴 ∪ 𝐴 ) |
| 9 | 5 6 8 | 3eqtri | ⊢ ∪ suc 𝐴 = ( ∪ 𝐴 ∪ 𝐴 ) |
| 10 | 9 | eqeq1i | ⊢ ( ∪ suc 𝐴 = 𝐴 ↔ ( ∪ 𝐴 ∪ 𝐴 ) = 𝐴 ) |
| 11 | 2 3 10 | 3bitr4i | ⊢ ( Tr 𝐴 ↔ ∪ suc 𝐴 = 𝐴 ) |