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 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
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 𝑃 )