Metamath Proof Explorer


Theorem fafv2elrn

Description: An alternate function value belongs to the codomain of the function, analogous to ffvelrn . (Contributed by AV, 2-Sep-2022)

Ref Expression
Assertion fafv2elrn ( ( 𝐹 : 𝐴𝐵𝐶𝐴 ) → ( 𝐹 '''' 𝐶 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ffn ( 𝐹 : 𝐴𝐵𝐹 Fn 𝐴 )
2 fnafv2elrn ( ( 𝐹 Fn 𝐴𝐶𝐴 ) → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 )
3 1 2 sylan ( ( 𝐹 : 𝐴𝐵𝐶𝐴 ) → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 )
4 frn ( 𝐹 : 𝐴𝐵 → ran 𝐹𝐵 )
5 4 sseld ( 𝐹 : 𝐴𝐵 → ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 → ( 𝐹 '''' 𝐶 ) ∈ 𝐵 ) )
6 5 adantr ( ( 𝐹 : 𝐴𝐵𝐶𝐴 ) → ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 → ( 𝐹 '''' 𝐶 ) ∈ 𝐵 ) )
7 3 6 mpd ( ( 𝐹 : 𝐴𝐵𝐶𝐴 ) → ( 𝐹 '''' 𝐶 ) ∈ 𝐵 )