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 𝑃 )