Theorem fcoresf1b

Description: A composition is injective iff the restrictions of its components to the minimum domains are injective. (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	fcoresf1b	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ↔ ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1→ 𝐷 ) ) )

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	⊢ ( ( 𝜑 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
8	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ) → 𝐺 : 𝐶 ⟶ 𝐷 )
9		simpr	⊢ ( ( 𝜑 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 )
10	7 2 3 4 8 6 9	fcoresf1	⊢ ( ( 𝜑 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ) → ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1→ 𝐷 ) )
11	10	ex	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 → ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1→ 𝐷 ) ) )
12		f1co	⊢ ( ( 𝑌 : 𝐸 –1-1→ 𝐷 ∧ 𝑋 : 𝑃 –1-1→ 𝐸 ) → ( 𝑌 ∘ 𝑋 ) : 𝑃 –1-1→ 𝐷 )
13	12	ancoms	⊢ ( ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1→ 𝐷 ) → ( 𝑌 ∘ 𝑋 ) : 𝑃 –1-1→ 𝐷 )
14	1 2 3 4 5 6	fcores	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) = ( 𝑌 ∘ 𝑋 ) )
15		f1eq1	⊢ ( ( 𝐺 ∘ 𝐹 ) = ( 𝑌 ∘ 𝑋 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ↔ ( 𝑌 ∘ 𝑋 ) : 𝑃 –1-1→ 𝐷 ) )
16	14 15	syl	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ↔ ( 𝑌 ∘ 𝑋 ) : 𝑃 –1-1→ 𝐷 ) )
17	13 16	imbitrrid	⊢ ( 𝜑 → ( ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1→ 𝐷 ) → ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ) )
18	11 17	impbid	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ↔ ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1→ 𝐷 ) ) )