Theorem dfsuccl4

Description: Alternate definition that incorporates the most desirable properties of the successor class. (Contributed by Peter Mazsa, 30-Jan-2026)

	Ref	Expression
Assertion	dfsuccl4	|- Suc = { n | E! m e. n ( m C_ n /\ suc m = n ) }

Proof

Step	Hyp	Ref	Expression
1		dfsuccl3	|- Suc = { n | E! m suc m = n }
2		sucidg	|- ( m e. _V -> m e. suc m )
3	2	elv	|- m e. suc m
4		eleq2	|- ( suc m = n -> ( m e. suc m <-> m e. n ) )
5	3 4	mpbii	|- ( suc m = n -> m e. n )
6		sssucid	|- m C_ suc m
7		sseq2	|- ( suc m = n -> ( m C_ suc m <-> m C_ n ) )
8	6 7	mpbii	|- ( suc m = n -> m C_ n )
9	5 8	jca	|- ( suc m = n -> ( m e. n /\ m C_ n ) )
10	9	pm4.71ri	|- ( suc m = n <-> ( ( m e. n /\ m C_ n ) /\ suc m = n ) )
11		df-3an	|- ( ( m e. n /\ m C_ n /\ suc m = n ) <-> ( ( m e. n /\ m C_ n ) /\ suc m = n ) )
12		3anass	|- ( ( m e. n /\ m C_ n /\ suc m = n ) <-> ( m e. n /\ ( m C_ n /\ suc m = n ) ) )
13	10 11 12	3bitr2i	|- ( suc m = n <-> ( m e. n /\ ( m C_ n /\ suc m = n ) ) )
14	13	eubii	|- ( E! m suc m = n <-> E! m ( m e. n /\ ( m C_ n /\ suc m = n ) ) )
15		df-reu	|- ( E! m e. n ( m C_ n /\ suc m = n ) <-> E! m ( m e. n /\ ( m C_ n /\ suc m = n ) ) )
16	14 15	bitr4i	|- ( E! m suc m = n <-> E! m e. n ( m C_ n /\ suc m = n ) )
17	16	abbii	|- { n | E! m suc m = n } = { n | E! m e. n ( m C_ n /\ suc m = n ) }
18	1 17	eqtri	|- Suc = { n | E! m e. n ( m C_ n /\ suc m = n ) }