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	$⊢ φ \to F : A ⟶ B$
	fcores.e	$⊢ E = ran F \cap C$
	fcores.p	$⊢ P = F^{-1} [C]$
	fcores.x	$⊢ X = {F ↾}_{P}$
	fcores.g	$⊢ φ \to G : C ⟶ D$
	fcores.y	$⊢ Y = {G ↾}_{E}$
	fcoresfo.s	$⊢ φ \to (G \circ F) : P \underset{onto}{⟶} D$
Assertion	fcoresfo	$⊢ φ \to Y : E \underset{onto}{⟶} D$

Proof

Step	Hyp	Ref	Expression
1		fcores.f	$⊢ φ \to F : A ⟶ B$
2		fcores.e	$⊢ E = ran F \cap C$
3		fcores.p	$⊢ P = F^{-1} [C]$
4		fcores.x	$⊢ X = {F ↾}_{P}$
5		fcores.g	$⊢ φ \to G : C ⟶ D$
6		fcores.y	$⊢ Y = {G ↾}_{E}$
7		fcoresfo.s	$⊢ φ \to (G \circ F) : P \underset{onto}{⟶} D$
8	2	a1i	$⊢ φ \to E = ran F \cap C$
9		inss2	$⊢ ran F \cap C \subseteq C$
10	8 9	eqsstrdi	$⊢ φ \to E \subseteq C$
11	5 10	fssresd	$⊢ φ \to ({G ↾}_{E}) : E ⟶ D$
12	6	feq1i	$⊢ Y : E ⟶ D \leftrightarrow ({G ↾}_{E}) : E ⟶ D$
13	11 12	sylibr	$⊢ φ \to Y : E ⟶ D$
14	1 2 3 4	fcoreslem3	$⊢ φ \to X : P \underset{onto}{⟶} E$
15		fof	$⊢ X : P \underset{onto}{⟶} E \to X : P ⟶ E$
16	14 15	syl	$⊢ φ \to X : P ⟶ E$
17	1 2 3 4 5 6	fcores	$⊢ φ \to G \circ F = Y \circ X$
18	17	eqcomd	$⊢ φ \to Y \circ X = G \circ F$
19		foeq1	$⊢ Y \circ X = G \circ F \to ((Y \circ X) : P \underset{onto}{⟶} D \leftrightarrow (G \circ F) : P \underset{onto}{⟶} D)$
20	18 19	syl	$⊢ φ \to ((Y \circ X) : P \underset{onto}{⟶} D \leftrightarrow (G \circ F) : P \underset{onto}{⟶} D)$
21	7 20	mpbird	$⊢ φ \to (Y \circ X) : P \underset{onto}{⟶} D$
22		foco2	$⊢ (Y : E ⟶ D \land X : P ⟶ E \land (Y \circ X) : P \underset{onto}{⟶} D) \to Y : E \underset{onto}{⟶} D$
23	13 16 21 22	syl3anc	$⊢ φ \to Y : E \underset{onto}{⟶} D$

Metamath Proof Explorer

Theorem fcoresfo

Proof