Theorem fcoreslem1

Description: Lemma 1 for fcores . (Contributed by AV, 17-Sep-2024)

	Ref	Expression
Hypotheses	fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
	fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
Assertion	fcoreslem1	⊢ ( 𝜑 → 𝑃 = ( ◡ 𝐹 “ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
3		fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
4	1	ffund	⊢ ( 𝜑 → Fun 𝐹 )
5		cnvimainrn	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ran 𝐹 ∩ 𝐶 ) ) = ( ◡ 𝐹 “ 𝐶 ) )
6	4 5	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ran 𝐹 ∩ 𝐶 ) ) = ( ◡ 𝐹 “ 𝐶 ) )
7	6	eqcomd	⊢ ( 𝜑 → ( ◡ 𝐹 “ 𝐶 ) = ( ◡ 𝐹 “ ( ran 𝐹 ∩ 𝐶 ) ) )
8	2	imaeq2i	⊢ ( ◡ 𝐹 “ 𝐸 ) = ( ◡ 𝐹 “ ( ran 𝐹 ∩ 𝐶 ) )
9	7 3 8	3eqtr4g	⊢ ( 𝜑 → 𝑃 = ( ◡ 𝐹 “ 𝐸 ) )