Theorem fafv2elcdm

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

	Ref	Expression
Assertion	fafv2elcdm	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}C\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		ffn	$$⊢F:A⟶B\to FFnA$$
2		fnafv2elrn	$$⊢\left(FFnA\wedge C\in A\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}C\right)\in \mathrm{ran}F$$
3	1 2	sylan	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}C\right)\in \mathrm{ran}F$$
4		frn	$$⊢F:A⟶B\to \mathrm{ran}F\subseteq B$$
5	4	sseld	$$⊢F:A⟶B\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}C\right)\in \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}C\right)\in B\right)$$
6	5	adantr	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}C\right)\in \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}C\right)\in B\right)$$
7	3 6	mpd	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}C\right)\in B$$