Theorem fcoreslem4

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

	Ref	Expression
Hypotheses	fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
	fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
	fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
	fcores.g	⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
	fcores.y	⊢ 𝑌 = ( 𝐺 ↾ 𝐸 )
Assertion	fcoreslem4	⊢ ( 𝜑 → ( 𝑌 ∘ 𝑋 ) Fn 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
3		fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
4		fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
5		fcores.g	⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
6		fcores.y	⊢ 𝑌 = ( 𝐺 ↾ 𝐸 )
7	5	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐶 )
8	2	a1i	⊢ ( 𝜑 → 𝐸 = ( ran 𝐹 ∩ 𝐶 ) )
9		inss2	⊢ ( ran 𝐹 ∩ 𝐶 ) ⊆ 𝐶
10	8 9	eqsstrdi	⊢ ( 𝜑 → 𝐸 ⊆ 𝐶 )
11	7 10	fnssresd	⊢ ( 𝜑 → ( 𝐺 ↾ 𝐸 ) Fn 𝐸 )
12	6	fneq1i	⊢ ( 𝑌 Fn 𝐸 ↔ ( 𝐺 ↾ 𝐸 ) Fn 𝐸 )
13	11 12	sylibr	⊢ ( 𝜑 → 𝑌 Fn 𝐸 )
14	1 2 3 4	fcoreslem3	⊢ ( 𝜑 → 𝑋 : 𝑃 –onto→ 𝐸 )
15		fofn	⊢ ( 𝑋 : 𝑃 –onto→ 𝐸 → 𝑋 Fn 𝑃 )
16	14 15	syl	⊢ ( 𝜑 → 𝑋 Fn 𝑃 )
17	1 2 3 4	fcoreslem2	⊢ ( 𝜑 → ran 𝑋 = 𝐸 )
18		eqimss	⊢ ( ran 𝑋 = 𝐸 → ran 𝑋 ⊆ 𝐸 )
19	17 18	syl	⊢ ( 𝜑 → ran 𝑋 ⊆ 𝐸 )
20		fnco	⊢ ( ( 𝑌 Fn 𝐸 ∧ 𝑋 Fn 𝑃 ∧ ran 𝑋 ⊆ 𝐸 ) → ( 𝑌 ∘ 𝑋 ) Fn 𝑃 )
21	13 16 19 20	syl3anc	⊢ ( 𝜑 → ( 𝑌 ∘ 𝑋 ) Fn 𝑃 )