Theorem fcoresfo

Description: If a composition is surjective, then the restriction of its first component to the minimum domain is surjective. (Contributed by AV, 17-Sep-2024)

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

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		fcoresfo.s	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 )
8	2	a1i	⊢ ( 𝜑 → 𝐸 = ( ran 𝐹 ∩ 𝐶 ) )
9		inss2	⊢ ( ran 𝐹 ∩ 𝐶 ) ⊆ 𝐶
10	8 9	eqsstrdi	⊢ ( 𝜑 → 𝐸 ⊆ 𝐶 )
11	5 10	fssresd	⊢ ( 𝜑 → ( 𝐺 ↾ 𝐸 ) : 𝐸 ⟶ 𝐷 )
12	6	feq1i	⊢ ( 𝑌 : 𝐸 ⟶ 𝐷 ↔ ( 𝐺 ↾ 𝐸 ) : 𝐸 ⟶ 𝐷 )
13	11 12	sylibr	⊢ ( 𝜑 → 𝑌 : 𝐸 ⟶ 𝐷 )
14	1 2 3 4	fcoreslem3	⊢ ( 𝜑 → 𝑋 : 𝑃 –onto→ 𝐸 )
15		fof	⊢ ( 𝑋 : 𝑃 –onto→ 𝐸 → 𝑋 : 𝑃 ⟶ 𝐸 )
16	14 15	syl	⊢ ( 𝜑 → 𝑋 : 𝑃 ⟶ 𝐸 )
17	1 2 3 4 5 6	fcores	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑌 ∘ 𝑋 ) )
18	17	eqcomd	⊢ ( 𝜑 → ( 𝑌 ∘ 𝑋 ) = ( 𝐺 ∘ 𝐹 ) )
19		foeq1	⊢ ( ( 𝑌 ∘ 𝑋 ) = ( 𝐺 ∘ 𝐹 ) → ( ( 𝑌 ∘ 𝑋 ) : 𝑃 –onto→ 𝐷 ↔ ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ) )
20	18 19	syl	⊢ ( 𝜑 → ( ( 𝑌 ∘ 𝑋 ) : 𝑃 –onto→ 𝐷 ↔ ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ) )
21	7 20	mpbird	⊢ ( 𝜑 → ( 𝑌 ∘ 𝑋 ) : 𝑃 –onto→ 𝐷 )
22		foco2	⊢ ( ( 𝑌 : 𝐸 ⟶ 𝐷 ∧ 𝑋 : 𝑃 ⟶ 𝐸 ∧ ( 𝑌 ∘ 𝑋 ) : 𝑃 –onto→ 𝐷 ) → 𝑌 : 𝐸 –onto→ 𝐷 )
23	13 16 21 22	syl3anc	⊢ ( 𝜑 → 𝑌 : 𝐸 –onto→ 𝐷 )