Metamath Proof Explorer

Theorem chfnrn

Description: The range of a choice function (a function that chooses an element from each member of its domain) is included in the union of its domain. (Contributed by NM, 31-Aug-1999)

		Ref	Expression
	Assertion	chfnrn	$⊢ (F Fn A \land \forall x \in A F (x) \in x) \to ran F \subseteq ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		fvelrnb	$⊢ F Fn A \to (y \in ran F \leftrightarrow \exists x \in A F (x) = y)$
2	1	biimpd	$⊢ F Fn A \to (y \in ran F \to \exists x \in A F (x) = y)$
3		eleq1	$⊢ F (x) = y \to (F (x) \in x \leftrightarrow y \in x)$
4	3	biimpcd	$⊢ F (x) \in x \to (F (x) = y \to y \in x)$
5	4	ralimi	$⊢ \forall x \in A F (x) \in x \to \forall x \in A (F (x) = y \to y \in x)$
6		rexim	$⊢ \forall x \in A (F (x) = y \to y \in x) \to (\exists x \in A F (x) = y \to \exists x \in A y \in x)$
7	5 6	syl	$⊢ \forall x \in A F (x) \in x \to (\exists x \in A F (x) = y \to \exists x \in A y \in x)$
8	2 7	sylan9	$⊢ (F Fn A \land \forall x \in A F (x) \in x) \to (y \in ran F \to \exists x \in A y \in x)$
9		eluni2	$⊢ y \in ⋃ A \leftrightarrow \exists x \in A y \in x$
10	8 9	imbitrrdi	$⊢ (F Fn A \land \forall x \in A F (x) \in x) \to (y \in ran F \to y \in ⋃ A)$
11	10	ssrdv	$⊢ (F Fn A \land \forall x \in A F (x) \in x) \to ran F \subseteq ⋃ A$