Theorem fimacnv

Description: The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007)

	Ref	Expression
Assertion	fimacnv	|- ( F : A --> B -> ( `' F " B ) = A )

Proof

Step	Hyp	Ref	Expression
1		imassrn	|- ( `' F " B ) C_ ran `' F
2		dfdm4	|- dom F = ran `' F
3		fdm	|- ( F : A --> B -> dom F = A )
4		ssid	|- A C_ A
5	3 4	eqsstrdi	|- ( F : A --> B -> dom F C_ A )
6	2 5	eqsstrrid	|- ( F : A --> B -> ran `' F C_ A )
7	1 6	sstrid	|- ( F : A --> B -> ( `' F " B ) C_ A )
8		fimass	|- ( F : A --> B -> ( F " A ) C_ B )
9		ffun	|- ( F : A --> B -> Fun F )
10	4 3	sseqtrrid	|- ( F : A --> B -> A C_ dom F )
11		funimass3	|- ( ( Fun F /\ A C_ dom F ) -> ( ( F " A ) C_ B <-> A C_ ( `' F " B ) ) )
12	9 10 11	syl2anc	|- ( F : A --> B -> ( ( F " A ) C_ B <-> A C_ ( `' F " B ) ) )
13	8 12	mpbid	|- ( F : A --> B -> A C_ ( `' F " B ) )
14	7 13	eqssd	|- ( F : A --> B -> ( `' F " B ) = A )