Description: A class is equal to its successor iff it is a proper class (assuming the Axiom of Regularity). (Contributed by NM, 9-Jul-2004) (Proof shortened by BJ, 16-Apr-2019) (Proof shortened by SN, 22-Apr-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sucprcreg | ⊢ ( ¬ 𝐴 ∈ V ↔ suc 𝐴 = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sucprc | ⊢ ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 ) | |
| 2 | elirr | ⊢ ¬ 𝐴 ∈ 𝐴 | |
| 3 | snssg | ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ 𝐴 ↔ { 𝐴 } ⊆ 𝐴 ) ) | |
| 4 | 2 3 | mtbii | ⊢ ( 𝐴 ∈ V → ¬ { 𝐴 } ⊆ 𝐴 ) |
| 5 | df-suc | ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } ) | |
| 6 | 5 | eqeq1i | ⊢ ( suc 𝐴 = 𝐴 ↔ ( 𝐴 ∪ { 𝐴 } ) = 𝐴 ) |
| 7 | ssequn2 | ⊢ ( { 𝐴 } ⊆ 𝐴 ↔ ( 𝐴 ∪ { 𝐴 } ) = 𝐴 ) | |
| 8 | 6 7 | sylbb2 | ⊢ ( suc 𝐴 = 𝐴 → { 𝐴 } ⊆ 𝐴 ) |
| 9 | 4 8 | nsyl3 | ⊢ ( suc 𝐴 = 𝐴 → ¬ 𝐴 ∈ V ) |
| 10 | 1 9 | impbii | ⊢ ( ¬ 𝐴 ∈ V ↔ suc 𝐴 = 𝐴 ) |