Metamath Proof Explorer


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 syl5ibr ( 𝜑 → ( ( 𝑋 : 𝑃1-1𝐸𝑌 : 𝐸1-1𝐷 ) → ( 𝐺𝐹 ) : 𝑃1-1𝐷 ) )
18 11 17 impbid ( 𝜑 → ( ( 𝐺𝐹 ) : 𝑃1-1𝐷 ↔ ( 𝑋 : 𝑃1-1𝐸𝑌 : 𝐸1-1𝐷 ) ) )