Theorem dfpre4

Description: Alternate definition of the predecessor of the N set. The ` ``' SucMap ` is just the "PreMap"; we did not define it because we do not expect to use it extensively in future (cf. the comments of df-sucmap ). (Contributed by Peter Mazsa, 26-Jan-2026)

	Ref	Expression
Assertion	dfpre4	⊢ ( 𝑁 ∈ 𝑉 → pre 𝑁 = ( ℩ 𝑚 𝑚 ∈ [ 𝑁 ] ◡ SucMap ) )

Proof

Step	Hyp	Ref	Expression
1		df-pre	⊢ pre 𝑁 = ( ℩ 𝑚 𝑚 ∈ Pred ( SucMap , dom SucMap , 𝑁 ) )
2		dfpred4	⊢ ( 𝑁 ∈ 𝑉 → Pred ( SucMap , dom SucMap , 𝑁 ) = [ 𝑁 ] ◡ ( SucMap ↾ dom SucMap ) )
3		relsucmap	⊢ Rel SucMap
4		dfrel5	⊢ ( Rel SucMap ↔ ( SucMap ↾ dom SucMap ) = SucMap )
5	3 4	mpbi	⊢ ( SucMap ↾ dom SucMap ) = SucMap
6	5	cnveqi	⊢ ◡ ( SucMap ↾ dom SucMap ) = ◡ SucMap
7	6	eceq2i	⊢ [ 𝑁 ] ◡ ( SucMap ↾ dom SucMap ) = [ 𝑁 ] ◡ SucMap
8	2 7	eqtrdi	⊢ ( 𝑁 ∈ 𝑉 → Pred ( SucMap , dom SucMap , 𝑁 ) = [ 𝑁 ] ◡ SucMap )
9	8	eleq2d	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑚 ∈ Pred ( SucMap , dom SucMap , 𝑁 ) ↔ 𝑚 ∈ [ 𝑁 ] ◡ SucMap ) )
10	9	iotabidv	⊢ ( 𝑁 ∈ 𝑉 → ( ℩ 𝑚 𝑚 ∈ Pred ( SucMap , dom SucMap , 𝑁 ) ) = ( ℩ 𝑚 𝑚 ∈ [ 𝑁 ] ◡ SucMap ) )
11	1 10	eqtrid	⊢ ( 𝑁 ∈ 𝑉 → pre 𝑁 = ( ℩ 𝑚 𝑚 ∈ [ 𝑁 ] ◡ SucMap ) )