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 𝐹 ) |
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 𝐹 ) |