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

Metamath Proof Explorer

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→ 𝐷 )