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