This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 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 𝐹 ⊆ ∪ 𝐴 )