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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sucprcreg | ⊢ ( ¬ 𝐴 ∈ V ↔ suc 𝐴 = 𝐴 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sucprc | ⊢ ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 ) | |
| 2 | elirr | ⊢ ¬ 𝐴 ∈ 𝐴 | |
| 3 | df-suc | ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } ) | |
| 4 | 3 | eqeq1i | ⊢ ( suc 𝐴 = 𝐴 ↔ ( 𝐴 ∪ { 𝐴 } ) = 𝐴 ) |
| 5 | ssequn2 | ⊢ ( { 𝐴 } ⊆ 𝐴 ↔ ( 𝐴 ∪ { 𝐴 } ) = 𝐴 ) | |
| 6 | 4 5 | sylbb2 | ⊢ ( suc 𝐴 = 𝐴 → { 𝐴 } ⊆ 𝐴 ) |
| 7 | snidg | ⊢ ( 𝐴 ∈ V → 𝐴 ∈ { 𝐴 } ) | |
| 8 | ssel2 | ⊢ ( ( { 𝐴 } ⊆ 𝐴 ∧ 𝐴 ∈ { 𝐴 } ) → 𝐴 ∈ 𝐴 ) | |
| 9 | 6 7 8 | syl2an | ⊢ ( ( suc 𝐴 = 𝐴 ∧ 𝐴 ∈ V ) → 𝐴 ∈ 𝐴 ) |
| 10 | 2 9 | mto | ⊢ ¬ ( suc 𝐴 = 𝐴 ∧ 𝐴 ∈ V ) |
| 11 | 10 | imnani | ⊢ ( suc 𝐴 = 𝐴 → ¬ 𝐴 ∈ V ) |
| 12 | 1 11 | impbii | ⊢ ( ¬ 𝐴 ∈ V ↔ suc 𝐴 = 𝐴 ) |