Theorem fcoreslem3

Description: Lemma 3 for fcores . (Contributed by AV, 13-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
3		fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
4		fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
5	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
6	2	a1i	⊢ ( 𝜑 → 𝐸 = ( ran 𝐹 ∩ 𝐶 ) )
7	3	a1i	⊢ ( 𝜑 → 𝑃 = ( ◡ 𝐹 “ 𝐶 ) )
8	5 6 7	rescnvimafod	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑃 ) : 𝑃 –onto→ 𝐸 )
9		foeq1	⊢ ( 𝑋 = ( 𝐹 ↾ 𝑃 ) → ( 𝑋 : 𝑃 –onto→ 𝐸 ↔ ( 𝐹 ↾ 𝑃 ) : 𝑃 –onto→ 𝐸 ) )
10	4 9	mp1i	⊢ ( 𝜑 → ( 𝑋 : 𝑃 –onto→ 𝐸 ↔ ( 𝐹 ↾ 𝑃 ) : 𝑃 –onto→ 𝐸 ) )
11	8 10	mpbird	⊢ ( 𝜑 → 𝑋 : 𝑃 –onto→ 𝐸 )