Metamath Proof Explorer

Theorem wdomimag

Description: A set is weakly dominant over its image under any function. (Contributed by Stefan O'Rear, 14-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)

		Ref	Expression
	Assertion	wdomimag	$⊢ (Fun F \land A \in V) \to F [A] ≼^{*} A$

Proof

Step	Hyp	Ref	Expression
1		funimaexg	$⊢ (Fun F \land A \in V) \to F [A] \in V$
2		wdomima2g	$⊢ (Fun F \land A \in V \land F [A] \in V) \to F [A] ≼^{*} A$
3	1 2	mpd3an3	$⊢ (Fun F \land A \in V) \to F [A] ≼^{*} A$