fcoresfob

Description: A composition is surjective iff the restriction of its first component to the minimum domain is surjective. (Contributed by GL and AV, 7-Oct-2024)

	Ref	Expression
Hypotheses	fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
	fcores.p	⊢ 𝑃 = ( ^◡ 𝐹 “ 𝐶 )
	fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
	fcores.g	⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
	fcores.y	⊢ 𝑌 = ( 𝐺 ↾ 𝐸 )
Assertion	fcoresfob	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ↔ 𝑌 : 𝐸 –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	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
8	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ) → 𝐺 : 𝐶 ⟶ 𝐷 )
9		simpr	⊢ ( ( 𝜑 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 )
10	7 2 3 4 8 6 9	fcoresfo	⊢ ( ( 𝜑 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ) → 𝑌 : 𝐸 –onto→ 𝐷 )
11	1 2 3 4	fcoreslem3	⊢ ( 𝜑 → 𝑋 : 𝑃 –onto→ 𝐸 )
12	11	anim1ci	⊢ ( ( 𝜑 ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) → ( 𝑌 : 𝐸 –onto→ 𝐷 ∧ 𝑋 : 𝑃 –onto→ 𝐸 ) )
13		foco	⊢ ( ( 𝑌 : 𝐸 –onto→ 𝐷 ∧ 𝑋 : 𝑃 –onto→ 𝐸 ) → ( 𝑌 ∘ 𝑋 ) : 𝑃 –onto→ 𝐷 )
14	12 13	syl	⊢ ( ( 𝜑 ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) → ( 𝑌 ∘ 𝑋 ) : 𝑃 –onto→ 𝐷 )
15	1 2 3 4 5 6	fcores	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑌 ∘ 𝑋 ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) = ( 𝑌 ∘ 𝑋 ) )
17		foeq1	⊢ ( ( 𝐺 ∘ 𝐹 ) = ( 𝑌 ∘ 𝑋 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ↔ ( 𝑌 ∘ 𝑋 ) : 𝑃 –onto→ 𝐷 ) )
18	16 17	syl	⊢ ( ( 𝜑 ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ↔ ( 𝑌 ∘ 𝑋 ) : 𝑃 –onto→ 𝐷 ) )
19	14 18	mpbird	⊢ ( ( 𝜑 ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 )
20	10 19	impbida	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ↔ 𝑌 : 𝐸 –onto→ 𝐷 ) )

Metamath Proof Explorer

Theorem fcoresfob

Proof