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	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐹 “ 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		imassrn	⊢ ( ◡ 𝐹 “ 𝐵 ) ⊆ ran ◡ 𝐹
2		dfdm4	⊢ dom 𝐹 = ran ◡ 𝐹
3		fdm	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
4		ssid	⊢ 𝐴 ⊆ 𝐴
5	3 4	eqsstrdi	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 ⊆ 𝐴 )
6	2 5	eqsstrrid	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ran ◡ 𝐹 ⊆ 𝐴 )
7	1 6	sstrid	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐹 “ 𝐵 ) ⊆ 𝐴 )
8		fimass	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 “ 𝐴 ) ⊆ 𝐵 )
9		ffun	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → Fun 𝐹 )
10	4 3	sseqtrrid	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐴 ⊆ dom 𝐹 )
11		funimass3	⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) ) )
12	9 10 11	syl2anc	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 “ 𝐴 ) ⊆ 𝐵 ↔ 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) ) )
13	8 12	mpbid	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐴 ⊆ ( ◡ 𝐹 “ 𝐵 ) )
14	7 13	eqssd	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ◡ 𝐹 “ 𝐵 ) = 𝐴 )