fsupprnfi

Description: Finite support implies finite range. (Contributed by Thierry Arnoux, 24-Jun-2024)

		Ref	Expression
	Assertion	fsupprnfi	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to ran F \in Fin$

Proof

Step	Hyp	Ref	Expression
1		snfi	$⊢ \{\underset{˙}{0}\} \in Fin$
2		simpll	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to Fun F$
3		simplr	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to F \in V$
4		simprl	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to \underset{˙}{0} \in W$
5		ressupprn	$⊢ (Fun F \land F \in V \land \underset{˙}{0} \in W) \to ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) = ran F ∖ \{\underset{˙}{0}\}$
6	2 3 4 5	syl3anc	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) = ran F ∖ \{\underset{˙}{0}\}$
7		simprr	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to {finSupp}_{\underset{˙}{0}} (F)$
8	7	fsuppimpd	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to F supp \underset{˙}{0} \in Fin$
9		suppssdm	$⊢ F supp \underset{˙}{0} \subseteq dom F$
10		ssdmres	$⊢ F supp \underset{˙}{0} \subseteq dom F \leftrightarrow dom ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) = F supp \underset{˙}{0}$
11	9 10	mpbi	$⊢ dom ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) = F supp \underset{˙}{0}$
12	2	funresd	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to Fun ({F ↾}_{{supp}_{\underset{˙}{0}} (F)})$
13		funforn	$⊢ Fun ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \leftrightarrow ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) : dom ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \underset{onto}{⟶} ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)})$
14	12 13	sylib	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) : dom ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \underset{onto}{⟶} ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)})$
15		foeq2	$⊢ dom ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) = F supp \underset{˙}{0} \to (({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) : dom ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \underset{onto}{⟶} ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \leftrightarrow ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) : F supp \underset{˙}{0} \underset{onto}{⟶} ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}))$
16	15	biimpa	$⊢ (dom ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) = F supp \underset{˙}{0} \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) : dom ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \underset{onto}{⟶} ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)})) \to ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) : F supp \underset{˙}{0} \underset{onto}{⟶} ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)})$
17	11 14 16	sylancr	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) : F supp \underset{˙}{0} \underset{onto}{⟶} ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)})$
18		fofi	$⊢ (F supp \underset{˙}{0} \in Fin \land ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) : F supp \underset{˙}{0} \underset{onto}{⟶} ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)})) \to ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \in Fin$
19	8 17 18	syl2anc	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to ran ({F ↾}_{{supp}_{\underset{˙}{0}} (F)}) \in Fin$
20	6 19	eqeltrrd	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to ran F ∖ \{\underset{˙}{0}\} \in Fin$
21		diffib	$⊢ \{\underset{˙}{0}\} \in Fin \to (ran F \in Fin \leftrightarrow ran F ∖ \{\underset{˙}{0}\} \in Fin)$
22	21	biimpar	$⊢ (\{\underset{˙}{0}\} \in Fin \land ran F ∖ \{\underset{˙}{0}\} \in Fin) \to ran F \in Fin$
23	1 20 22	sylancr	$⊢ ((Fun F \land F \in V) \land (\underset{˙}{0} \in W \land {finSupp}_{\underset{˙}{0}} (F))) \to ran F \in Fin$

Metamath Proof Explorer

Theorem fsupprnfi

Proof