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