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

Metamath Proof Explorer

Theorem fconst2g

Description: A constant function expressed as a Cartesian product. (Contributed by NM, 27-Nov-2007)

Ref Expression
Assertion fconst2g 
|- ( B e. C -> ( F : A --> { B } <-> F = ( A X. { B } ) ) )

Proof

Step Hyp Ref Expression
1 fvconst 
 |-  ( ( F : A --> { B } /\ x e. A ) -> ( F ` x ) = B )
2 1 adantlr 
 |-  ( ( ( F : A --> { B } /\ B e. C ) /\ x e. A ) -> ( F ` x ) = B )
3 fvconst2g 
 |-  ( ( B e. C /\ x e. A ) -> ( ( A X. { B } ) ` x ) = B )
4 3 adantll 
 |-  ( ( ( F : A --> { B } /\ B e. C ) /\ x e. A ) -> ( ( A X. { B } ) ` x ) = B )
5 2 4 eqtr4d 
 |-  ( ( ( F : A --> { B } /\ B e. C ) /\ x e. A ) -> ( F ` x ) = ( ( A X. { B } ) ` x ) )
6 5 ralrimiva 
 |-  ( ( F : A --> { B } /\ B e. C ) -> A. x e. A ( F ` x ) = ( ( A X. { B } ) ` x ) )
7 ffn 
 |-  ( F : A --> { B } -> F Fn A )
8 fnconstg 
 |-  ( B e. C -> ( A X. { B } ) Fn A )
9 eqfnfv 
 |-  ( ( F Fn A /\ ( A X. { B } ) Fn A ) -> ( F = ( A X. { B } ) <-> A. x e. A ( F ` x ) = ( ( A X. { B } ) ` x ) ) )
10 7 8 9 syl2an 
 |-  ( ( F : A --> { B } /\ B e. C ) -> ( F = ( A X. { B } ) <-> A. x e. A ( F ` x ) = ( ( A X. { B } ) ` x ) ) )
11 6 10 mpbird 
 |-  ( ( F : A --> { B } /\ B e. C ) -> F = ( A X. { B } ) )
12 11 expcom 
 |-  ( B e. C -> ( F : A --> { B } -> F = ( A X. { B } ) ) )
13 fconstg 
 |-  ( B e. C -> ( A X. { B } ) : A --> { B } )
14 feq1 
 |-  ( F = ( A X. { B } ) -> ( F : A --> { B } <-> ( A X. { B } ) : A --> { B } ) )
15 13 14 syl5ibrcom 
 |-  ( B e. C -> ( F = ( A X. { B } ) -> F : A --> { B } ) )
16 12 15 impbid 
 |-  ( B e. C -> ( F : A --> { B } <-> F = ( A X. { B } ) ) )