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

Metamath Proof Explorer

Theorem fconst5

Description: Two ways to express that a function is constant. (Contributed by NM, 27-Nov-2007)

Ref Expression
Assertion fconst5 
|- ( ( F Fn A /\ A =/= (/) ) -> ( F = ( A X. { B } ) <-> ran F = { B } ) )

Proof

Step Hyp Ref Expression
1 rneq 
 |-  ( F = ( A X. { B } ) -> ran F = ran ( A X. { B } ) )
2 rnxp 
 |-  ( A =/= (/) -> ran ( A X. { B } ) = { B } )
3 2 eqeq2d 
 |-  ( A =/= (/) -> ( ran F = ran ( A X. { B } ) <-> ran F = { B } ) )
4 1 3 imbitrid 
 |-  ( A =/= (/) -> ( F = ( A X. { B } ) -> ran F = { B } ) )
5 4 adantl 
 |-  ( ( F Fn A /\ A =/= (/) ) -> ( F = ( A X. { B } ) -> ran F = { B } ) )
6 df-fo 
 |-  ( F : A -onto-> { B } <-> ( F Fn A /\ ran F = { B } ) )
7 fof 
 |-  ( F : A -onto-> { B } -> F : A --> { B } )
8 6 7 sylbir 
 |-  ( ( F Fn A /\ ran F = { B } ) -> F : A --> { B } )
9 fconst2g 
 |-  ( B e. _V -> ( F : A --> { B } <-> F = ( A X. { B } ) ) )
10 8 9 imbitrid 
 |-  ( B e. _V -> ( ( F Fn A /\ ran F = { B } ) -> F = ( A X. { B } ) ) )
11 10 expd 
 |-  ( B e. _V -> ( F Fn A -> ( ran F = { B } -> F = ( A X. { B } ) ) ) )
12 11 adantrd 
 |-  ( B e. _V -> ( ( F Fn A /\ A =/= (/) ) -> ( ran F = { B } -> F = ( A X. { B } ) ) ) )
13 fnrel 
 |-  ( F Fn A -> Rel F )
14 snprc 
 |-  ( -. B e. _V <-> { B } = (/) )
15 relrn0 
 |-  ( Rel F -> ( F = (/) <-> ran F = (/) ) )
16 15 biimprd 
 |-  ( Rel F -> ( ran F = (/) -> F = (/) ) )
17 16 adantl 
 |-  ( ( { B } = (/) /\ Rel F ) -> ( ran F = (/) -> F = (/) ) )
18 eqeq2 
 |-  ( { B } = (/) -> ( ran F = { B } <-> ran F = (/) ) )
19 18 adantr 
 |-  ( ( { B } = (/) /\ Rel F ) -> ( ran F = { B } <-> ran F = (/) ) )
20 xpeq2 
 |-  ( { B } = (/) -> ( A X. { B } ) = ( A X. (/) ) )
21 xp0 
 |-  ( A X. (/) ) = (/)
22 20 21 eqtrdi 
 |-  ( { B } = (/) -> ( A X. { B } ) = (/) )
23 22 eqeq2d 
 |-  ( { B } = (/) -> ( F = ( A X. { B } ) <-> F = (/) ) )
24 23 adantr 
 |-  ( ( { B } = (/) /\ Rel F ) -> ( F = ( A X. { B } ) <-> F = (/) ) )
25 17 19 24 3imtr4d 
 |-  ( ( { B } = (/) /\ Rel F ) -> ( ran F = { B } -> F = ( A X. { B } ) ) )
26 25 ex 
 |-  ( { B } = (/) -> ( Rel F -> ( ran F = { B } -> F = ( A X. { B } ) ) ) )
27 14 26 sylbi 
 |-  ( -. B e. _V -> ( Rel F -> ( ran F = { B } -> F = ( A X. { B } ) ) ) )
28 13 27 syl5 
 |-  ( -. B e. _V -> ( F Fn A -> ( ran F = { B } -> F = ( A X. { B } ) ) ) )
29 28 adantrd 
 |-  ( -. B e. _V -> ( ( F Fn A /\ A =/= (/) ) -> ( ran F = { B } -> F = ( A X. { B } ) ) ) )
30 12 29 pm2.61i 
 |-  ( ( F Fn A /\ A =/= (/) ) -> ( ran F = { B } -> F = ( A X. { B } ) ) )
31 5 30 impbid 
 |-  ( ( F Fn A /\ A =/= (/) ) -> ( F = ( A X. { B } ) <-> ran F = { B } ) )