# Metamath Proof Explorer

## Theorem funsseq

Description: Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012) (Proof shortened by Mario Carneiro, 3-May-2015)

Ref Expression
Assertion funsseq ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\wedge \mathrm{dom}{F}=\mathrm{dom}{G}\right)\to \left({F}={G}↔{F}\subseteq {G}\right)$

### Proof

Step Hyp Ref Expression
1 eqimss ${⊢}{F}={G}\to {F}\subseteq {G}$
2 simpl3 ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\wedge \mathrm{dom}{F}=\mathrm{dom}{G}\right)\wedge {F}\subseteq {G}\right)\to \mathrm{dom}{F}=\mathrm{dom}{G}$
3 2 reseq2d ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\wedge \mathrm{dom}{F}=\mathrm{dom}{G}\right)\wedge {F}\subseteq {G}\right)\to {{G}↾}_{\mathrm{dom}{F}}={{G}↾}_{\mathrm{dom}{G}}$
4 funssres ${⊢}\left(\mathrm{Fun}{G}\wedge {F}\subseteq {G}\right)\to {{G}↾}_{\mathrm{dom}{F}}={F}$
5 4 3ad2antl2 ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\wedge \mathrm{dom}{F}=\mathrm{dom}{G}\right)\wedge {F}\subseteq {G}\right)\to {{G}↾}_{\mathrm{dom}{F}}={F}$
6 simpl2 ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\wedge \mathrm{dom}{F}=\mathrm{dom}{G}\right)\wedge {F}\subseteq {G}\right)\to \mathrm{Fun}{G}$
7 funrel ${⊢}\mathrm{Fun}{G}\to \mathrm{Rel}{G}$
8 resdm ${⊢}\mathrm{Rel}{G}\to {{G}↾}_{\mathrm{dom}{G}}={G}$
9 6 7 8 3syl ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\wedge \mathrm{dom}{F}=\mathrm{dom}{G}\right)\wedge {F}\subseteq {G}\right)\to {{G}↾}_{\mathrm{dom}{G}}={G}$
10 3 5 9 3eqtr3d ${⊢}\left(\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\wedge \mathrm{dom}{F}=\mathrm{dom}{G}\right)\wedge {F}\subseteq {G}\right)\to {F}={G}$
11 10 ex ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\wedge \mathrm{dom}{F}=\mathrm{dom}{G}\right)\to \left({F}\subseteq {G}\to {F}={G}\right)$
12 1 11 impbid2 ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{Fun}{G}\wedge \mathrm{dom}{F}=\mathrm{dom}{G}\right)\to \left({F}={G}↔{F}\subseteq {G}\right)$