imadomg

Description: An image of a function under a set is dominated by the set. Proposition 10.34 of TakeutiZaring p. 92. (Contributed by NM, 23-Jul-2004)

		Ref	Expression
	Assertion	imadomg	$⊢ A \in B \to (Fun F \to F [A] ≼ A)$

Proof

Step	Hyp	Ref	Expression
1		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
2		resfunexg	$⊢ (Fun F \land A \in B) \to {F ↾}_{A} \in V$
3	2	dmexd	$⊢ (Fun F \land A \in B) \to dom ({F ↾}_{A}) \in V$
4		funres	$⊢ Fun F \to Fun ({F ↾}_{A})$
5		funforn	$⊢ Fun ({F ↾}_{A}) \leftrightarrow ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})$
6	4 5	sylib	$⊢ Fun F \to ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})$
7	6	adantr	$⊢ (Fun F \land A \in B) \to ({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A})$
8		fodomg	$⊢ dom ({F ↾}_{A}) \in V \to (({F ↾}_{A}) : dom ({F ↾}_{A}) \underset{onto}{⟶} ran ({F ↾}_{A}) \to ran ({F ↾}_{A}) ≼ dom ({F ↾}_{A}))$
9	3 7 8	sylc	$⊢ (Fun F \land A \in B) \to ran ({F ↾}_{A}) ≼ dom ({F ↾}_{A})$
10	1 9	eqbrtrid	$⊢ (Fun F \land A \in B) \to F [A] ≼ dom ({F ↾}_{A})$
11	10	expcom	$⊢ A \in B \to (Fun F \to F [A] ≼ dom ({F ↾}_{A}))$
12		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
13		inss1	$⊢ A \cap dom F \subseteq A$
14	12 13	eqsstri	$⊢ dom ({F ↾}_{A}) \subseteq A$
15		ssdomg	$⊢ A \in B \to (dom ({F ↾}_{A}) \subseteq A \to dom ({F ↾}_{A}) ≼ A)$
16	14 15	mpi	$⊢ A \in B \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 B) \to F [A] ≼ A$
19	18	expcom	$⊢ A \in B \to (F [A] ≼ dom ({F ↾}_{A}) \to F [A] ≼ A)$
20	11 19	syld	$⊢ A \in B \to (Fun F \to F [A] ≼ A)$

Metamath Proof Explorer

Theorem imadomg

Proof