Metamath Proof Explorer


Theorem fcoresf1ob

Description: A composition is bijective iff the restriction of its first component to the minimum domain is bijective and the restriction of its second component to the minimum domain is 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 fcoresf1ob ( 𝜑 → ( ( 𝐺𝐹 ) : 𝑃1-1-onto𝐷 ↔ ( 𝑋 : 𝑃1-1𝐸𝑌 : 𝐸1-1-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 2 3 4 5 6 fcoresf1b ( 𝜑 → ( ( 𝐺𝐹 ) : 𝑃1-1𝐷 ↔ ( 𝑋 : 𝑃1-1𝐸𝑌 : 𝐸1-1𝐷 ) ) )
8 1 2 3 4 5 6 fcoresfob ( 𝜑 → ( ( 𝐺𝐹 ) : 𝑃onto𝐷𝑌 : 𝐸onto𝐷 ) )
9 7 8 anbi12d ( 𝜑 → ( ( ( 𝐺𝐹 ) : 𝑃1-1𝐷 ∧ ( 𝐺𝐹 ) : 𝑃onto𝐷 ) ↔ ( ( 𝑋 : 𝑃1-1𝐸𝑌 : 𝐸1-1𝐷 ) ∧ 𝑌 : 𝐸onto𝐷 ) ) )
10 anass ( ( ( 𝑋 : 𝑃1-1𝐸𝑌 : 𝐸1-1𝐷 ) ∧ 𝑌 : 𝐸onto𝐷 ) ↔ ( 𝑋 : 𝑃1-1𝐸 ∧ ( 𝑌 : 𝐸1-1𝐷𝑌 : 𝐸onto𝐷 ) ) )
11 9 10 bitrdi ( 𝜑 → ( ( ( 𝐺𝐹 ) : 𝑃1-1𝐷 ∧ ( 𝐺𝐹 ) : 𝑃onto𝐷 ) ↔ ( 𝑋 : 𝑃1-1𝐸 ∧ ( 𝑌 : 𝐸1-1𝐷𝑌 : 𝐸onto𝐷 ) ) ) )
12 df-f1o ( ( 𝐺𝐹 ) : 𝑃1-1-onto𝐷 ↔ ( ( 𝐺𝐹 ) : 𝑃1-1𝐷 ∧ ( 𝐺𝐹 ) : 𝑃onto𝐷 ) )
13 df-f1o ( 𝑌 : 𝐸1-1-onto𝐷 ↔ ( 𝑌 : 𝐸1-1𝐷𝑌 : 𝐸onto𝐷 ) )
14 13 anbi2i ( ( 𝑋 : 𝑃1-1𝐸𝑌 : 𝐸1-1-onto𝐷 ) ↔ ( 𝑋 : 𝑃1-1𝐸 ∧ ( 𝑌 : 𝐸1-1𝐷𝑌 : 𝐸onto𝐷 ) ) )
15 11 12 14 3bitr4g ( 𝜑 → ( ( 𝐺𝐹 ) : 𝑃1-1-onto𝐷 ↔ ( 𝑋 : 𝑃1-1𝐸𝑌 : 𝐸1-1-onto𝐷 ) ) )