Metamath Proof Explorer

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	Could not format assertion : No typesetting found for \|- Suc = { n \| E! m e. n ( m C_ n /\ suc m = n ) } with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		dfsuccl3	Could not format Suc = { n \| E! m suc m = n } : No typesetting found for \|- Suc = { n \| E! m suc m = n } with typecode \|-
2		sucidg	$⊢ m \in V \to m \in suc m$
3	2	elv	$⊢ m \in suc m$
4		eleq2	$⊢ suc m = n \to (m \in suc m \leftrightarrow m \in n)$
5	3 4	mpbii	$⊢ suc m = n \to m \in n$
6		sssucid	$⊢ m \subseteq suc m$
7		sseq2	$⊢ suc m = n \to (m \subseteq suc m \leftrightarrow m \subseteq n)$
8	6 7	mpbii	$⊢ suc m = n \to m \subseteq n$
9	5 8	jca	$⊢ suc m = n \to (m \in n \land m \subseteq n)$
10	9	pm4.71ri	$⊢ suc m = n \leftrightarrow ((m \in n \land m \subseteq n) \land suc m = n)$
11		df-3an	$⊢ (m \in n \land m \subseteq n \land suc m = n) \leftrightarrow ((m \in n \land m \subseteq n) \land suc m = n)$
12		3anass	$⊢ (m \in n \land m \subseteq n \land suc m = n) \leftrightarrow (m \in n \land (m \subseteq n \land suc m = n))$
13	10 11 12	3bitr2i	$⊢ suc m = n \leftrightarrow (m \in n \land (m \subseteq n \land suc m = n))$
14	13	eubii	$⊢ \exists! m suc m = n \leftrightarrow \exists! m (m \in n \land (m \subseteq n \land suc m = n))$
15		df-reu	$⊢ \exists! m \in n (m \subseteq n \land suc m = n) \leftrightarrow \exists! m (m \in n \land (m \subseteq n \land suc m = n))$
16	14 15	bitr4i	$⊢ \exists! m suc m = n \leftrightarrow \exists! m \in n (m \subseteq n \land suc m = n)$
17	16	abbii	$⊢ \{n \| \exists! m suc m = n\} = \{n \| \exists! m \in n (m \subseteq n \land suc m = n)\}$
18	1 17	eqtri	Could not format Suc = { n \| E! m e. n ( m C_ n /\ suc m = n ) } : No typesetting found for \|- Suc = { n \| E! m e. n ( m C_ n /\ suc m = n ) } with typecode \|-