Description: The range of a function is dominated by its domain. (Contributed by NM, 1-Sep-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | fnrndomg | ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐹 Fn 𝐴 → ran 𝐹 ≼ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dffn4 | ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 ) | |
2 | fodomg | ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐹 : 𝐴 –onto→ ran 𝐹 → ran 𝐹 ≼ 𝐴 ) ) | |
3 | 1 2 | syl5bi | ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐹 Fn 𝐴 → ran 𝐹 ≼ 𝐴 ) ) |