imadomfi

Description: An image of a function under a finite set is dominated by the set. (Contributed by SN, 10-May-2025)

		Ref	Expression
	Assertion	imadomfi	$⊢ (A \in Fin \land Fun F) \to F [A] ≼ A$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
2		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
3		resfnfinfin	$⊢ (F Fn dom F \land A \in Fin) \to {F ↾}_{A} \in Fin$
4	2 3	sylanb	$⊢ (Fun F \land A \in Fin) \to {F ↾}_{A} \in Fin$
5		dmfi	$⊢ {F ↾}_{A} \in Fin \to dom ({F ↾}_{A}) \in Fin$
6	4 5	syl	$⊢ (Fun F \land A \in Fin) \to dom ({F ↾}_{A}) \in Fin$
7		funres	$⊢ Fun F \to Fun ({F ↾}_{A})$
8		funforn	$⊢ Fun ({F ↾}_{A}) \leftrightarrow ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})$
9	7 8	sylib	$⊢ Fun F \to ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})$
10	9	adantr	$⊢ (Fun F \land A \in Fin) \to ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})$
11		fodomfi	$⊢ (dom ({F ↾}_{A}) \in Fin \land ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})) \to ran ({F ↾}_{A}) ≼ dom ({F ↾}_{A})$
12	6 10 11	syl2anc	$⊢ (Fun F \land A \in Fin) \to ran ({F ↾}_{A}) ≼ dom ({F ↾}_{A})$
13	1 12	eqbrtrid	$⊢ (Fun F \land A \in Fin) \to F [A] ≼ dom ({F ↾}_{A})$
14		resdmss	$⊢ dom ({F ↾}_{A}) \subseteq A$
15		ssdomfi	$⊢ A \in Fin \to (dom ({F ↾}_{A}) \subseteq A \to dom ({F ↾}_{A}) ≼ A)$
16	14 15	mpi	$⊢ A \in Fin \to dom ({F ↾}_{A}) ≼ A$
17		domtr	$⊢ (F [A] ≼ dom ({F ↾}_{A}) \land dom ({F ↾}_{A}) ≼ A) \to F [A] ≼ A$
18	16 17	sylan2	$⊢ (F [A] ≼ dom ({F ↾}_{A}) \land A \in Fin) \to F [A] ≼ A$
19	13 18	sylancom	$⊢ (Fun F \land A \in Fin) \to F [A] ≼ A$
20	19	ancoms	$⊢ (A \in Fin \land Fun F) \to F [A] ≼ A$

Metamath Proof Explorer

Theorem imadomfi

Proof