Theorem fcoreslem2

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

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

Proof

Step	Hyp	Ref	Expression
1		fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
3		fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
4		fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
5		df-ima	⊢ ( 𝐹 “ 𝑃 ) = ran ( 𝐹 ↾ 𝑃 )
6	4	rneqi	⊢ ran 𝑋 = ran ( 𝐹 ↾ 𝑃 )
7	6	eqcomi	⊢ ran ( 𝐹 ↾ 𝑃 ) = ran 𝑋
8	7	a1i	⊢ ( 𝜑 → ran ( 𝐹 ↾ 𝑃 ) = ran 𝑋 )
9	5 8	eqtr2id	⊢ ( 𝜑 → ran 𝑋 = ( 𝐹 “ 𝑃 ) )
10	1 2 3	fcoreslem1	⊢ ( 𝜑 → 𝑃 = ( ◡ 𝐹 “ 𝐸 ) )
11	10	imaeq2d	⊢ ( 𝜑 → ( 𝐹 “ 𝑃 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝐸 ) ) )
12	1	ffund	⊢ ( 𝜑 → Fun 𝐹 )
13		funimacnv	⊢ ( Fun 𝐹 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐸 ) ) = ( 𝐸 ∩ ran 𝐹 ) )
14	12 13	syl	⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐸 ) ) = ( 𝐸 ∩ ran 𝐹 ) )
15		inss1	⊢ ( ran 𝐹 ∩ 𝐶 ) ⊆ ran 𝐹
16	2 15	eqsstri	⊢ 𝐸 ⊆ ran 𝐹
17	16	a1i	⊢ ( 𝜑 → 𝐸 ⊆ ran 𝐹 )
18		dfss2	⊢ ( 𝐸 ⊆ ran 𝐹 ↔ ( 𝐸 ∩ ran 𝐹 ) = 𝐸 )
19	17 18	sylib	⊢ ( 𝜑 → ( 𝐸 ∩ ran 𝐹 ) = 𝐸 )
20	14 19	eqtrd	⊢ ( 𝜑 → ( 𝐹 “ ( ◡ 𝐹 “ 𝐸 ) ) = 𝐸 )
21	9 11 20	3eqtrd	⊢ ( 𝜑 → ran 𝑋 = 𝐸 )