Theorem fconst4

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

	Ref	Expression
Assertion	fconst4	|- ( F : A --> { B } <-> ( F Fn A /\ ( `' F " { B } ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		fconst3	|- ( F : A --> { B } <-> ( F Fn A /\ A C_ ( `' F " { B } ) ) )
2		cnvimass	|- ( `' F " { B } ) C_ dom F
3		fndm	|- ( F Fn A -> dom F = A )
4	2 3	sseqtrid	|- ( F Fn A -> ( `' F " { B } ) C_ A )
5	4	biantrurd	|- ( F Fn A -> ( A C_ ( `' F " { B } ) <-> ( ( `' F " { B } ) C_ A /\ A C_ ( `' F " { B } ) ) ) )
6		eqss	|- ( ( `' F " { B } ) = A <-> ( ( `' F " { B } ) C_ A /\ A C_ ( `' F " { B } ) ) )
7	5 6	bitr4di	|- ( F Fn A -> ( A C_ ( `' F " { B } ) <-> ( `' F " { B } ) = A ) )
8	7	pm5.32i	|- ( ( F Fn A /\ A C_ ( `' F " { B } ) ) <-> ( F Fn A /\ ( `' F " { B } ) = A ) )
9	1 8	bitri	|- ( F : A --> { B } <-> ( F Fn A /\ ( `' F " { B } ) = A ) )