Metamath Proof Explorer


Theorem ndmafv2nrn

Description: The value of a class outside its domain is not in the range, compare with ndmfv . (Contributed by AV, 2-Sep-2022)

Ref Expression
Assertion ndmafv2nrn ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 orc ( ¬ 𝐴 ∈ dom 𝐹 → ( ¬ 𝐴 ∈ dom 𝐹 ∨ ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
2 ianor ( ¬ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) ↔ ( ¬ 𝐴 ∈ dom 𝐹 ∨ ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
3 df-dfat ( 𝐹 defAt 𝐴 ↔ ( 𝐴 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
4 2 3 xchnxbir ( ¬ 𝐹 defAt 𝐴 ↔ ( ¬ 𝐴 ∈ dom 𝐹 ∨ ¬ Fun ( 𝐹 ↾ { 𝐴 } ) ) )
5 1 4 sylibr ( ¬ 𝐴 ∈ dom 𝐹 → ¬ 𝐹 defAt 𝐴 )
6 ndfatafv2nrn ( ¬ 𝐹 defAt 𝐴 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )
7 5 6 syl ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 '''' 𝐴 ) ∉ ran 𝐹 )