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

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 ⁡ F ∧ Fun ⁡ G ∧ F ↾ X = G ↾ X ∧ X ∈ dom ⁡ F ∧ X ∈ dom ⁡ G ∧ F ⁡ X = G ⁡ X → F ↾ suc ⁡ X = G ↾ suc ⁡ X

Proof

Step Hyp Ref Expression
1 eqfunresadj ⊢ Fun ⁡ F ∧ Fun ⁡ G ∧ F ↾ X = G ↾ X ∧ X ∈ dom ⁡ F ∧ X ∈ dom ⁡ G ∧ F ⁡ X = G ⁡ X → F ↾ X ∪ X = G ↾ X ∪ X
2 df-suc ⊢ suc ⁡ X = X ∪ X
3 2 reseq2i ⊢ F ↾ suc ⁡ X = F ↾ X ∪ X
4 2 reseq2i ⊢ G ↾ suc ⁡ X = G ↾ X ∪ X
5 1 3 4 3eqtr4g ⊢ Fun ⁡ F ∧ Fun ⁡ G ∧ F ↾ X = G ↾ X ∧ X ∈ dom ⁡ F ∧ X ∈ dom ⁡ G ∧ F ⁡ X = G ⁡ X → F ↾ suc ⁡ X = G ↾ suc ⁡ X