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

Metamath Proof Explorer

Theorem f1ocoima

Description: The composition of two bijections as bijection onto the image of the range of the first bijection. (Contributed by AV, 15-Aug-2025)

Ref Expression
Assertion f1ocoima ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ B ⊆ C → G ∘ F : A ⟶ 1-1 onto G B

Proof

Step Hyp Ref Expression
1 f1of1 ⊢ G : C ⟶ 1-1 onto D → G : C ⟶ 1-1 D
2 1 anim1i ⊢ G : C ⟶ 1-1 onto D ∧ B ⊆ C → G : C ⟶ 1-1 D ∧ B ⊆ C
3 2 3adant1 ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ B ⊆ C → G : C ⟶ 1-1 D ∧ B ⊆ C
4 f1ores ⊢ G : C ⟶ 1-1 D ∧ B ⊆ C → G ↾ B : B ⟶ 1-1 onto G B
5 3 4 syl ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ B ⊆ C → G ↾ B : B ⟶ 1-1 onto G B
6 simp1 ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ B ⊆ C → F : A ⟶ 1-1 onto B
7 f1oco ⊢ G ↾ B : B ⟶ 1-1 onto G B ∧ F : A ⟶ 1-1 onto B → G ↾ B ∘ F : A ⟶ 1-1 onto G B
8 5 6 7 syl2anc ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ B ⊆ C → G ↾ B ∘ F : A ⟶ 1-1 onto G B
9 f1ofo ⊢ F : A ⟶ 1-1 onto B → F : A ⟶ onto B
10 forn ⊢ F : A ⟶ onto B → ran ⁡ F = B
11 9 10 syl ⊢ F : A ⟶ 1-1 onto B → ran ⁡ F = B
12 11 eqimssd ⊢ F : A ⟶ 1-1 onto B → ran ⁡ F ⊆ B
13 12 3ad2ant1 ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ B ⊆ C → ran ⁡ F ⊆ B
14 cores ⊢ ran ⁡ F ⊆ B → G ↾ B ∘ F = G ∘ F
15 14 eqcomd ⊢ ran ⁡ F ⊆ B → G ∘ F = G ↾ B ∘ F
16 13 15 syl ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ B ⊆ C → G ∘ F = G ↾ B ∘ F
17 16 f1oeq1d ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ B ⊆ C → G ∘ F : A ⟶ 1-1 onto G B ↔ G ↾ B ∘ F : A ⟶ 1-1 onto G B
18 8 17 mpbird ⊢ F : A ⟶ 1-1 onto B ∧ G : C ⟶ 1-1 onto D ∧ B ⊆ C → G ∘ F : A ⟶ 1-1 onto G B