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

Metamath Proof Explorer

Theorem fconst7v

Description: An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022) Removed hyphotheses as suggested by SN (Revised by Thierry Arnoux, 10-Jan-2026)

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

Proof

Step Hyp Ref Expression
1 fconst7v.f 
 |-  ( ph -> F Fn A )
2 fconst7v.e 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) = B )
3 0xp 
 |-  ( (/) X. { B } ) = (/)
4 3 a1i 
 |-  ( ( ph /\ A = (/) ) -> ( (/) X. { B } ) = (/) )
5 simpr 
 |-  ( ( ph /\ A = (/) ) -> A = (/) )
6 5 xpeq1d 
 |-  ( ( ph /\ A = (/) ) -> ( A X. { B } ) = ( (/) X. { B } ) )
7 1 adantr 
 |-  ( ( ph /\ A = (/) ) -> F Fn A )
8 fneq2 
 |-  ( A = (/) -> ( F Fn A <-> F Fn (/) ) )
9 8 adantl 
 |-  ( ( ph /\ A = (/) ) -> ( F Fn A <-> F Fn (/) ) )
10 7 9 mpbid 
 |-  ( ( ph /\ A = (/) ) -> F Fn (/) )
11 fn0 
 |-  ( F Fn (/) <-> F = (/) )
12 10 11 sylib 
 |-  ( ( ph /\ A = (/) ) -> F = (/) )
13 4 6 12 3eqtr4rd 
 |-  ( ( ph /\ A = (/) ) -> F = ( A X. { B } ) )
14 fvexd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. _V )
15 2 14 eqeltrrd 
 |-  ( ( ph /\ x e. A ) -> B e. _V )
16 snidg 
 |-  ( B e. _V -> B e. { B } )
17 15 16 syl 
 |-  ( ( ph /\ x e. A ) -> B e. { B } )
18 2 17 eqeltrd 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. { B } )
19 18 ralrimiva 
 |-  ( ph -> A. x e. A ( F ` x ) e. { B } )
20 nfcv 
 |-  F/_ x A
21 nfcv 
 |-  F/_ x { B }
22 nfcv 
 |-  F/_ x F
23 20 21 22 ffnfvf 
 |-  ( F : A --> { B } <-> ( F Fn A /\ A. x e. A ( F ` x ) e. { B } ) )
24 1 19 23 sylanbrc 
 |-  ( ph -> F : A --> { B } )
25 24 adantr 
 |-  ( ( ph /\ A =/= (/) ) -> F : A --> { B } )
26 simpr 
 |-  ( ( ph /\ A =/= (/) ) -> A =/= (/) )
27 15 adantlr 
 |-  ( ( ( ph /\ A =/= (/) ) /\ x e. A ) -> B e. _V )
28 26 27 n0limd 
 |-  ( ( ph /\ A =/= (/) ) -> B e. _V )
29 fconst2g 
 |-  ( B e. _V -> ( F : A --> { B } <-> F = ( A X. { B } ) ) )
30 28 29 syl 
 |-  ( ( ph /\ A =/= (/) ) -> ( F : A --> { B } <-> F = ( A X. { B } ) ) )
31 25 30 mpbid 
 |-  ( ( ph /\ A =/= (/) ) -> F = ( A X. { B } ) )
32 exmidne 
 |-  ( A = (/) \/ A =/= (/) )
33 32 a1i 
 |-  ( ph -> ( A = (/) \/ A =/= (/) ) )
34 13 31 33 mpjaodan 
 |-  ( ph -> F = ( A X. { B } ) )