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

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