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	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝑥 ) → ran 𝐹 ⊆ ∪ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fvelrnb	⊢ ( 𝐹 Fn 𝐴 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
2	1	biimpd	⊢ ( 𝐹 Fn 𝐴 → ( 𝑦 ∈ ran 𝐹 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
3		eleq1	⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
4	3	biimpcd	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑥 → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝑥 ) )
5	4	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝑥 → ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝑥 ) )
6		rexim	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ 𝑥 ) → ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ) )
7	5 6	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝑥 → ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ) )
8	2 7	sylan9	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝑥 ) → ( 𝑦 ∈ ran 𝐹 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 ) )
9		eluni2	⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 )
10	8 9	imbitrrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝑥 ) → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ ∪ 𝐴 ) )
11	10	ssrdv	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝑥 ) → ran 𝐹 ⊆ ∪ 𝐴 )