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	$⊢ \neg A \in dom F \to (F'''' A) \notin ran F$

Step	Hyp	Ref	Expression
1		orc	$⊢ \neg A \in dom F \to (\neg A \in dom F \lor \neg Fun ({F ↾}_{\{A\}}))$
2		ianor	$⊢ \neg (A \in dom F \land Fun ({F ↾}_{\{A\}})) \leftrightarrow (\neg A \in dom F \lor \neg Fun ({F ↾}_{\{A\}}))$
3		df-dfat	$⊢ F defAt A \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
4	2 3	xchnxbir	$⊢ \neg F defAt A \leftrightarrow (\neg A \in dom F \lor \neg Fun ({F ↾}_{\{A\}}))$
5	1 4	sylibr	$⊢ \neg A \in dom F \to \neg F defAt A$
6		ndfatafv2nrn	$⊢ \neg F defAt A \to (F'''' A) \notin ran F$
7	5 6	syl	$⊢ \neg A \in dom F \to (F'''' A) \notin ran F$

Metamath Proof Explorer