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	$⊢ (Fun F \land Fun G \land dom F = dom G) \to (F = G \leftrightarrow F \subseteq G)$

Proof

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