Theorem fimacnvdisj

Description: The preimage of a class disjoint with a mapping's codomain is empty. (Contributed by FL, 24-Jan-2007)

	Ref	Expression
Assertion	fimacnvdisj	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → ( ◡ 𝐹 “ 𝐶 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝐹 = dom ◡ 𝐹
2		frn	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ran 𝐹 ⊆ 𝐵 )
3	2	adantr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → ran 𝐹 ⊆ 𝐵 )
4	1 3	eqsstrrid	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → dom ◡ 𝐹 ⊆ 𝐵 )
5		ssdisj	⊢ ( ( dom ◡ 𝐹 ⊆ 𝐵 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → ( dom ◡ 𝐹 ∩ 𝐶 ) = ∅ )
6	4 5	sylancom	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → ( dom ◡ 𝐹 ∩ 𝐶 ) = ∅ )
7		imadisj	⊢ ( ( ◡ 𝐹 “ 𝐶 ) = ∅ ↔ ( dom ◡ 𝐹 ∩ 𝐶 ) = ∅ )
8	6 7	sylibr	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → ( ◡ 𝐹 “ 𝐶 ) = ∅ )