fsuppres

Description: The restriction of a finitely supported function is finitely supported. (Contributed by AV, 14-Jul-2019)

	Ref	Expression
Hypotheses	fsuppres.s	$⊢ φ \to {finSupp}_{Z} (F)$
	fsuppres.z	$⊢ φ \to Z \in V$
Assertion	fsuppres	$⊢ φ \to {finSupp}_{Z} (({F ↾}_{X}))$

Proof

Step	Hyp	Ref	Expression
1		fsuppres.s	$⊢ φ \to {finSupp}_{Z} (F)$
2		fsuppres.z	$⊢ φ \to Z \in V$
3		fsuppimp	$⊢ {finSupp}_{Z} (F) \to (Fun F \land F supp Z \in Fin)$
4		relprcnfsupp	$⊢ \neg F \in V \to \neg {finSupp}_{Z} (F)$
5	4	con4i	$⊢ {finSupp}_{Z} (F) \to F \in V$
6	1 5	syl	$⊢ φ \to F \in V$
7	6 2	jca	$⊢ φ \to (F \in V \land Z \in V)$
8	7	adantr	$⊢ (φ \land Fun F) \to (F \in V \land Z \in V)$
9		ressuppss	$⊢ (F \in V \land Z \in V) \to ({F ↾}_{X}) supp Z \subseteq F supp Z$
10		ssfi	$⊢ (F supp Z \in Fin \land ({F ↾}_{X}) supp Z \subseteq F supp Z) \to ({F ↾}_{X}) supp Z \in Fin$
11	10	expcom	$⊢ ({F ↾}_{X}) supp Z \subseteq F supp Z \to (F supp Z \in Fin \to ({F ↾}_{X}) supp Z \in Fin)$
12	8 9 11	3syl	$⊢ (φ \land Fun F) \to (F supp Z \in Fin \to ({F ↾}_{X}) supp Z \in Fin)$
13	12	expcom	$⊢ Fun F \to (φ \to (F supp Z \in Fin \to ({F ↾}_{X}) supp Z \in Fin))$
14	13	com23	$⊢ Fun F \to (F supp Z \in Fin \to (φ \to ({F ↾}_{X}) supp Z \in Fin))$
15	14	imp	$⊢ (Fun F \land F supp Z \in Fin) \to (φ \to ({F ↾}_{X}) supp Z \in Fin)$
16	3 15	syl	$⊢ {finSupp}_{Z} (F) \to (φ \to ({F ↾}_{X}) supp Z \in Fin)$
17	1 16	mpcom	$⊢ φ \to ({F ↾}_{X}) supp Z \in Fin$
18		funres	$⊢ Fun F \to Fun ({F ↾}_{X})$
19	18	adantr	$⊢ (Fun F \land F supp Z \in Fin) \to Fun ({F ↾}_{X})$
20	1 3 19	3syl	$⊢ φ \to Fun ({F ↾}_{X})$
21		resexg	$⊢ F \in V \to {F ↾}_{X} \in V$
22	1 5 21	3syl	$⊢ φ \to {F ↾}_{X} \in V$
23		funisfsupp	$⊢ (Fun ({F ↾}_{X}) \land {F ↾}_{X} \in V \land Z \in V) \to ({finSupp}_{Z} (({F ↾}_{X})) \leftrightarrow ({F ↾}_{X}) supp Z \in Fin)$
24	20 22 2 23	syl3anc	$⊢ φ \to ({finSupp}_{Z} (({F ↾}_{X})) \leftrightarrow ({F ↾}_{X}) supp Z \in Fin)$
25	17 24	mpbird	$⊢ φ \to {finSupp}_{Z} (({F ↾}_{X}))$

Metamath Proof Explorer

Theorem fsuppres

Proof