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