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

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 ⊢ φ → F : A ⟶ B
fcores.e ⊢ E = ran ⁡ F ∩ C
fcores.p ⊢ P = F -1 C
fcores.x ⊢ X = F ↾ P
fcores.g ⊢ φ → G : C ⟶ D
fcores.y ⊢ Y = G ↾ E
Assertion fcoresf1ob ⊢ φ → G ∘ F : P ⟶ 1-1 onto D ↔ X : P ⟶ 1-1 E ∧ Y : E ⟶ 1-1 onto D

Proof

Step Hyp Ref Expression
1 fcores.f ⊢ φ → F : A ⟶ B
2 fcores.e ⊢ E = ran ⁡ F ∩ C
3 fcores.p ⊢ P = F -1 C
4 fcores.x ⊢ X = F ↾ P
5 fcores.g ⊢ φ → G : C ⟶ D
6 fcores.y ⊢ Y = G ↾ E
7 1 2 3 4 5 6 fcoresf1b ⊢ φ → G ∘ F : P ⟶ 1-1 D ↔ X : P ⟶ 1-1 E ∧ Y : E ⟶ 1-1 D
8 1 2 3 4 5 6 fcoresfob ⊢ φ → G ∘ F : P ⟶ onto D ↔ Y : E ⟶ onto D
9 7 8 anbi12d ⊢ φ → G ∘ F : P ⟶ 1-1 D ∧ G ∘ F : P ⟶ onto D ↔ X : P ⟶ 1-1 E ∧ Y : E ⟶ 1-1 D ∧ Y : E ⟶ onto D
10 anass ⊢ X : P ⟶ 1-1 E ∧ Y : E ⟶ 1-1 D ∧ Y : E ⟶ onto D ↔ X : P ⟶ 1-1 E ∧ Y : E ⟶ 1-1 D ∧ Y : E ⟶ onto D
11 9 10 bitrdi ⊢ φ → G ∘ F : P ⟶ 1-1 D ∧ G ∘ F : P ⟶ onto D ↔ X : P ⟶ 1-1 E ∧ Y : E ⟶ 1-1 D ∧ Y : E ⟶ onto D
12 df-f1o ⊢ G ∘ F : P ⟶ 1-1 onto D ↔ G ∘ F : P ⟶ 1-1 D ∧ G ∘ F : P ⟶ onto D
13 df-f1o ⊢ Y : E ⟶ 1-1 onto D ↔ Y : E ⟶ 1-1 D ∧ Y : E ⟶ onto D
14 13 anbi2i ⊢ X : P ⟶ 1-1 E ∧ Y : E ⟶ 1-1 onto D ↔ X : P ⟶ 1-1 E ∧ Y : E ⟶ 1-1 D ∧ Y : E ⟶ onto D
15 11 12 14 3bitr4g ⊢ φ → G ∘ F : P ⟶ 1-1 onto D ↔ X : P ⟶ 1-1 E ∧ Y : E ⟶ 1-1 onto D