Metamath Proof Explorer


Theorem eqfunressuc

Description: Law for equality of restriction to successors. This is primarily useful when X is an ordinal, but it does not require that. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion eqfunressuc ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹𝑋 ) = ( 𝐺𝑋 ) ∧ ( 𝑋 ∈ dom 𝐹𝑋 ∈ dom 𝐺 ∧ ( 𝐹𝑋 ) = ( 𝐺𝑋 ) ) ) → ( 𝐹 ↾ suc 𝑋 ) = ( 𝐺 ↾ suc 𝑋 ) )

Proof

Step Hyp Ref Expression
1 eqfunresadj ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹𝑋 ) = ( 𝐺𝑋 ) ∧ ( 𝑋 ∈ dom 𝐹𝑋 ∈ dom 𝐺 ∧ ( 𝐹𝑋 ) = ( 𝐺𝑋 ) ) ) → ( 𝐹 ↾ ( 𝑋 ∪ { 𝑋 } ) ) = ( 𝐺 ↾ ( 𝑋 ∪ { 𝑋 } ) ) )
2 df-suc suc 𝑋 = ( 𝑋 ∪ { 𝑋 } )
3 2 reseq2i ( 𝐹 ↾ suc 𝑋 ) = ( 𝐹 ↾ ( 𝑋 ∪ { 𝑋 } ) )
4 2 reseq2i ( 𝐺 ↾ suc 𝑋 ) = ( 𝐺 ↾ ( 𝑋 ∪ { 𝑋 } ) )
5 1 3 4 3eqtr4g ( ( ( Fun 𝐹 ∧ Fun 𝐺 ) ∧ ( 𝐹𝑋 ) = ( 𝐺𝑋 ) ∧ ( 𝑋 ∈ dom 𝐹𝑋 ∈ dom 𝐺 ∧ ( 𝐹𝑋 ) = ( 𝐺𝑋 ) ) ) → ( 𝐹 ↾ suc 𝑋 ) = ( 𝐺 ↾ suc 𝑋 ) )