This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )