funssres

Description: The restriction of a function to the domain of a subclass equals the subclass. (Contributed by NM, 15-Aug-1994)

		Ref	Expression
	Assertion	funssres	$⊢ (Fun F \land G \subseteq F) \to {F ↾}_{dom G} = G$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ y \in V$
2	1	opelresi	$⊢ ⟨x, y⟩ \in ({F ↾}_{dom G}) \leftrightarrow (x \in dom G \land ⟨x, y⟩ \in F)$
3		vex	$⊢ x \in V$
4	3 1	opeldm	$⊢ ⟨x, y⟩ \in G \to x \in dom G$
5	4	a1i	$⊢ G \subseteq F \to (⟨x, y⟩ \in G \to x \in dom G)$
6		ssel	$⊢ G \subseteq F \to (⟨x, y⟩ \in G \to ⟨x, y⟩ \in F)$
7	5 6	jcad	$⊢ G \subseteq F \to (⟨x, y⟩ \in G \to (x \in dom G \land ⟨x, y⟩ \in F))$
8	7	adantl	$⊢ (Fun F \land G \subseteq F) \to (⟨x, y⟩ \in G \to (x \in dom G \land ⟨x, y⟩ \in F))$
9		funeu2	$⊢ (Fun F \land ⟨x, y⟩ \in F) \to \exists! y ⟨x, y⟩ \in F$
10	3	eldm2	$⊢ x \in dom G \leftrightarrow \exists y ⟨x, y⟩ \in G$
11	6	ancrd	$⊢ G \subseteq F \to (⟨x, y⟩ \in G \to (⟨x, y⟩ \in F \land ⟨x, y⟩ \in G))$
12	11	eximdv	$⊢ G \subseteq F \to (\exists y ⟨x, y⟩ \in G \to \exists y (⟨x, y⟩ \in F \land ⟨x, y⟩ \in G))$
13	10 12	syl5bi	$⊢ G \subseteq F \to (x \in dom G \to \exists y (⟨x, y⟩ \in F \land ⟨x, y⟩ \in G))$
14	13	imp	$⊢ (G \subseteq F \land x \in dom G) \to \exists y (⟨x, y⟩ \in F \land ⟨x, y⟩ \in G)$
15		eupick	$⊢ (\exists! y ⟨x, y⟩ \in F \land \exists y (⟨x, y⟩ \in F \land ⟨x, y⟩ \in G)) \to (⟨x, y⟩ \in F \to ⟨x, y⟩ \in G)$
16	9 14 15	syl2an	$⊢ ((Fun F \land ⟨x, y⟩ \in F) \land (G \subseteq F \land x \in dom G)) \to (⟨x, y⟩ \in F \to ⟨x, y⟩ \in G)$
17	16	exp43	$⊢ Fun F \to (⟨x, y⟩ \in F \to (G \subseteq F \to (x \in dom G \to (⟨x, y⟩ \in F \to ⟨x, y⟩ \in G))))$
18	17	com23	$⊢ Fun F \to (G \subseteq F \to (⟨x, y⟩ \in F \to (x \in dom G \to (⟨x, y⟩ \in F \to ⟨x, y⟩ \in G))))$
19	18	imp	$⊢ (Fun F \land G \subseteq F) \to (⟨x, y⟩ \in F \to (x \in dom G \to (⟨x, y⟩ \in F \to ⟨x, y⟩ \in G)))$
20	19	com34	$⊢ (Fun F \land G \subseteq F) \to (⟨x, y⟩ \in F \to (⟨x, y⟩ \in F \to (x \in dom G \to ⟨x, y⟩ \in G)))$
21	20	pm2.43d	$⊢ (Fun F \land G \subseteq F) \to (⟨x, y⟩ \in F \to (x \in dom G \to ⟨x, y⟩ \in G))$
22	21	impcomd	$⊢ (Fun F \land G \subseteq F) \to ((x \in dom G \land ⟨x, y⟩ \in F) \to ⟨x, y⟩ \in G)$
23	8 22	impbid	$⊢ (Fun F \land G \subseteq F) \to (⟨x, y⟩ \in G \leftrightarrow (x \in dom G \land ⟨x, y⟩ \in F))$
24	2 23	bitr4id	$⊢ (Fun F \land G \subseteq F) \to (⟨x, y⟩ \in ({F ↾}_{dom G}) \leftrightarrow ⟨x, y⟩ \in G)$
25	24	alrimivv	$⊢ (Fun F \land G \subseteq F) \to \forall x \forall y (⟨x, y⟩ \in ({F ↾}_{dom G}) \leftrightarrow ⟨x, y⟩ \in G)$
26		relres	$⊢ Rel ({F ↾}_{dom G})$
27		funrel	$⊢ Fun F \to Rel F$
28		relss	$⊢ G \subseteq F \to (Rel F \to Rel G)$
29	27 28	mpan9	$⊢ (Fun F \land G \subseteq F) \to Rel G$
30		eqrel	$⊢ (Rel ({F ↾}_{dom G}) \land Rel G) \to ({F ↾}_{dom G} = G \leftrightarrow \forall x \forall y (⟨x, y⟩ \in ({F ↾}_{dom G}) \leftrightarrow ⟨x, y⟩ \in G))$
31	26 29 30	sylancr	$⊢ (Fun F \land G \subseteq F) \to ({F ↾}_{dom G} = G \leftrightarrow \forall x \forall y (⟨x, y⟩ \in ({F ↾}_{dom G}) \leftrightarrow ⟨x, y⟩ \in G))$
32	25 31	mpbird	$⊢ (Fun F \land G \subseteq F) \to {F ↾}_{dom G} = G$

Metamath Proof Explorer

Theorem funssres

Proof