This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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