pmresg

Description: Elementhood of a restricted function in the set of partial functions. (Contributed by Mario Carneiro, 31-Dec-2013)

		Ref	Expression
	Assertion	pmresg	$⊢ (B \in V \land F \in (A ↑_{𝑝𝑚} C)) \to {F ↾}_{B} \in (A ↑_{𝑝𝑚} B)$

Proof

Step	Hyp	Ref	Expression
1		n0i	$⊢ F \in (A ↑_{𝑝𝑚} C) \to \neg A ↑_{𝑝𝑚} C = \emptyset$
2		fnpm	$⊢ ↑_{𝑝𝑚} Fn (V \times V)$
3	2	fndmi	$⊢ dom ↑_{𝑝𝑚} = V \times V$
4	3	ndmov	$⊢ \neg (A \in V \land C \in V) \to A ↑_{𝑝𝑚} C = \emptyset$
5	1 4	nsyl2	$⊢ F \in (A ↑_{𝑝𝑚} C) \to (A \in V \land C \in V)$
6	5	simpld	$⊢ F \in (A ↑_{𝑝𝑚} C) \to A \in V$
7	6	adantl	$⊢ (B \in V \land F \in (A ↑_{𝑝𝑚} C)) \to A \in V$
8		simpl	$⊢ (B \in V \land F \in (A ↑_{𝑝𝑚} C)) \to B \in V$
9		elpmi	$⊢ F \in (A ↑_{𝑝𝑚} C) \to (F : dom F ⟶ A \land dom F \subseteq C)$
10	9	simpld	$⊢ F \in (A ↑_{𝑝𝑚} C) \to F : dom F ⟶ A$
11	10	adantl	$⊢ (B \in V \land F \in (A ↑_{𝑝𝑚} C)) \to F : dom F ⟶ A$
12		inss1	$⊢ dom F \cap B \subseteq dom F$
13		fssres	$⊢ (F : dom F ⟶ A \land dom F \cap B \subseteq dom F) \to ({F ↾}_{(dom F \cap B)}) : dom F \cap B ⟶ A$
14	11 12 13	sylancl	$⊢ (B \in V \land F \in (A ↑_{𝑝𝑚} C)) \to ({F ↾}_{(dom F \cap B)}) : dom F \cap B ⟶ A$
15		ffun	$⊢ F : dom F ⟶ A \to Fun F$
16		resres	$⊢ {({F ↾}_{dom F}) ↾}_{B} = {F ↾}_{(dom F \cap B)}$
17		funrel	$⊢ Fun F \to Rel F$
18		resdm	$⊢ Rel F \to {F ↾}_{dom F} = F$
19		reseq1	$⊢ {F ↾}_{dom F} = F \to {({F ↾}_{dom F}) ↾}_{B} = {F ↾}_{B}$
20	17 18 19	3syl	$⊢ Fun F \to {({F ↾}_{dom F}) ↾}_{B} = {F ↾}_{B}$
21	16 20	eqtr3id	$⊢ Fun F \to {F ↾}_{(dom F \cap B)} = {F ↾}_{B}$
22	11 15 21	3syl	$⊢ (B \in V \land F \in (A ↑_{𝑝𝑚} C)) \to {F ↾}_{(dom F \cap B)} = {F ↾}_{B}$
23	22	feq1d	$⊢ (B \in V \land F \in (A ↑_{𝑝𝑚} C)) \to (({F ↾}_{(dom F \cap B)}) : dom F \cap B ⟶ A \leftrightarrow ({F ↾}_{B}) : dom F \cap B ⟶ A)$
24	14 23	mpbid	$⊢ (B \in V \land F \in (A ↑_{𝑝𝑚} C)) \to ({F ↾}_{B}) : dom F \cap B ⟶ A$
25		inss2	$⊢ dom F \cap B \subseteq B$
26		elpm2r	$⊢ ((A \in V \land B \in V) \land (({F ↾}_{B}) : dom F \cap B ⟶ A \land dom F \cap B \subseteq B)) \to {F ↾}_{B} \in (A ↑_{𝑝𝑚} B)$
27	25 26	mpanr2	$⊢ ((A \in V \land B \in V) \land ({F ↾}_{B}) : dom F \cap B ⟶ A) \to {F ↾}_{B} \in (A ↑_{𝑝𝑚} B)$
28	7 8 24 27	syl21anc	$⊢ (B \in V \land F \in (A ↑_{𝑝𝑚} C)) \to {F ↾}_{B} \in (A ↑_{𝑝𝑚} B)$

Metamath Proof Explorer

Theorem pmresg

Proof