Theorem fconst4

Description: Two ways to express a constant function. (Contributed by NM, 8-Mar-2007)

	Ref	Expression
Assertion	fconst4	$$⊢F:A⟶\left\{B\right\}\leftrightarrow \left(FFnA\wedge F^{-1}\left[\left\{B\right\}\right]=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		fconst3	$$⊢F:A⟶\left\{B\right\}\leftrightarrow \left(FFnA\wedge A\subseteq F^{-1}\left[\left\{B\right\}\right]\right)$$
2		cnvimass	$$⊢F^{-1}\left[\left\{B\right\}\right]\subseteq \mathrm{dom}F$$
3		fndm	$$⊢FFnA\to \mathrm{dom}F=A$$
4	2 3	sseqtrid	$$⊢FFnA\to F^{-1}\left[\left\{B\right\}\right]\subseteq A$$
5	4	biantrurd	$$⊢FFnA\to \left(A\subseteq F^{-1}\left[\left\{B\right\}\right]\leftrightarrow \left(F^{-1}\left[\left\{B\right\}\right]\subseteq A\wedge A\subseteq F^{-1}\left[\left\{B\right\}\right]\right)\right)$$
6		eqss	$$⊢F^{-1}\left[\left\{B\right\}\right]=A\leftrightarrow \left(F^{-1}\left[\left\{B\right\}\right]\subseteq A\wedge A\subseteq F^{-1}\left[\left\{B\right\}\right]\right)$$
7	5 6	bitr4di	$$⊢FFnA\to \left(A\subseteq F^{-1}\left[\left\{B\right\}\right]\leftrightarrow F^{-1}\left[\left\{B\right\}\right]=A\right)$$
8	7	pm5.32i	$$⊢\left(FFnA\wedge A\subseteq F^{-1}\left[\left\{B\right\}\right]\right)\leftrightarrow \left(FFnA\wedge F^{-1}\left[\left\{B\right\}\right]=A\right)$$
9	1 8	bitri	$$⊢F:A⟶\left\{B\right\}\leftrightarrow \left(FFnA\wedge F^{-1}\left[\left\{B\right\}\right]=A\right)$$