Metamath Proof Explorer


Theorem fafv2elrnb

Description: An alternate function value is defined, i.e., belongs to the range of the function, iff its argument is in the domain of the function. (Contributed by AV, 3-Sep-2022)

Ref Expression
Assertion fafv2elrnb ( 𝐹 : 𝐴𝐵 → ( 𝐶𝐴 ↔ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ffn ( 𝐹 : 𝐴𝐵𝐹 Fn 𝐴 )
2 fnafv2elrn ( ( 𝐹 Fn 𝐴𝐶𝐴 ) → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 )
3 1 2 sylan ( ( 𝐹 : 𝐴𝐵𝐶𝐴 ) → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 )
4 3 ex ( 𝐹 : 𝐴𝐵 → ( 𝐶𝐴 → ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) )
5 fdm ( 𝐹 : 𝐴𝐵 → dom 𝐹 = 𝐴 )
6 ndmafv2nrn ( ¬ 𝐶 ∈ dom 𝐹 → ( 𝐹 '''' 𝐶 ) ∉ ran 𝐹 )
7 df-nel ( ( 𝐹 '''' 𝐶 ) ∉ ran 𝐹 ↔ ¬ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 )
8 6 7 sylib ( ¬ 𝐶 ∈ dom 𝐹 → ¬ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 )
9 8 con4i ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹𝐶 ∈ dom 𝐹 )
10 eleq2 ( dom 𝐹 = 𝐴 → ( 𝐶 ∈ dom 𝐹𝐶𝐴 ) )
11 9 10 syl5ib ( dom 𝐹 = 𝐴 → ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹𝐶𝐴 ) )
12 5 11 syl ( 𝐹 : 𝐴𝐵 → ( ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹𝐶𝐴 ) )
13 4 12 impbid ( 𝐹 : 𝐴𝐵 → ( 𝐶𝐴 ↔ ( 𝐹 '''' 𝐶 ) ∈ ran 𝐹 ) )