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

Metamath Proof Explorer

Theorem fconst7

Description: An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses fconst7.p 
|- F/ x ph
fconst7.x 
|- F/_ x F
fconst7.f 
|- ( ph -> F Fn A )
fconst7.b 
|- ( ph -> B e. V )
fconst7.e 
|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
Assertion fconst7 
|- ( ph -> F = ( A X. { B } ) )

Proof

Step Hyp Ref Expression
1 fconst7.p 
 |-  F/ x ph
2 fconst7.x 
 |-  F/_ x F
3 fconst7.f 
 |-  ( ph -> F Fn A )
4 fconst7.b 
 |-  ( ph -> B e. V )
5 fconst7.e 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = B )
6 fvexd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. _V )
7 5 6 eqeltrrd 
 |-  ( ( ph /\ x e. A ) -> B e. _V )
8 snidg 
 |-  ( B e. _V -> B e. { B } )
9 7 8 syl 
 |-  ( ( ph /\ x e. A ) -> B e. { B } )
10 5 9 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. { B } )
11 1 10 ralrimia 
 |-  ( ph -> A. x e. A ( F ` x ) e. { B } )
12 nfcv 
 |-  F/_ x A
13 nfcv 
 |-  F/_ x { B }
14 12 13 2 ffnfvf 
 |-  ( F : A --> { B } <-> ( F Fn A /\ A. x e. A ( F ` x ) e. { B } ) )
15 3 11 14 sylanbrc 
 |-  ( ph -> F : A --> { B } )
16 fconst2g 
 |-  ( B e. V -> ( F : A --> { B } <-> F = ( A X. { B } ) ) )
17 4 16 syl 
 |-  ( ph -> ( F : A --> { B } <-> F = ( A X. { B } ) ) )
18 15 17 mpbid 
 |-  ( ph -> F = ( A X. { B } ) )