This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fcoreslem4

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

Ref Expression
Hypotheses fcores.f ⊢ φ → F : A ⟶ B
fcores.e ⊢ E = ran ⁡ F ∩ C
fcores.p ⊢ P = F -1 C
fcores.x ⊢ X = F ↾ P
fcores.g ⊢ φ → G : C ⟶ D
fcores.y ⊢ Y = G ↾ E
Assertion fcoreslem4 ⊢ φ → Y ∘ X Fn P

Proof

Step Hyp Ref Expression
1 fcores.f ⊢ φ → F : A ⟶ B
2 fcores.e ⊢ E = ran ⁡ F ∩ C
3 fcores.p ⊢ P = F -1 C
4 fcores.x ⊢ X = F ↾ P
5 fcores.g ⊢ φ → G : C ⟶ D
6 fcores.y ⊢ Y = G ↾ E
7 5 ffnd ⊢ φ → G Fn C
8 2 a1i ⊢ φ → E = ran ⁡ F ∩ C
9 inss2 ⊢ ran ⁡ F ∩ C ⊆ C
10 8 9 eqsstrdi ⊢ φ → E ⊆ C
11 7 10 fnssresd ⊢ φ → G ↾ E Fn E
12 6 fneq1i ⊢ Y Fn E ↔ G ↾ E Fn E
13 11 12 sylibr ⊢ φ → Y Fn E
14 1 2 3 4 fcoreslem3 ⊢ φ → X : P ⟶ onto E
15 fofn ⊢ X : P ⟶ onto E → X Fn P
16 14 15 syl ⊢ φ → X Fn P
17 1 2 3 4 fcoreslem2 ⊢ φ → ran ⁡ X = E
18 eqimss ⊢ ran ⁡ X = E → ran ⁡ X ⊆ E
19 17 18 syl ⊢ φ → ran ⁡ X ⊆ E
20 fnco ⊢ Y Fn E ∧ X Fn P ∧ ran ⁡ X ⊆ E → Y ∘ X Fn P
21 13 16 19 20 syl3anc ⊢ φ → Y ∘ X Fn P