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 \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land B \subseteq C) \to (G \circ F) : A \underset{1-1 onto}{⟶} G [B]$

Proof

Step	Hyp	Ref	Expression
1		f1of1	$⊢ G : C \underset{1-1 onto}{⟶} D \to G : C \underset{1-1}{⟶} D$
2	1	anim1i	$⊢ (G : C \underset{1-1 onto}{⟶} D \land B \subseteq C) \to (G : C \underset{1-1}{⟶} D \land B \subseteq C)$
3	2	3adant1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land B \subseteq C) \to (G : C \underset{1-1}{⟶} D \land B \subseteq C)$
4		f1ores	$⊢ (G : C \underset{1-1}{⟶} D \land B \subseteq C) \to ({G ↾}_{B}) : B \underset{1-1 onto}{⟶} G [B]$
5	3 4	syl	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land B \subseteq C) \to ({G ↾}_{B}) : B \underset{1-1 onto}{⟶} G [B]$
6		simp1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land B \subseteq C) \to F : A \underset{1-1 onto}{⟶} B$
7		f1oco	$⊢ (({G ↾}_{B}) : B \underset{1-1 onto}{⟶} G [B] \land F : A \underset{1-1 onto}{⟶} B) \to (({G ↾}_{B}) \circ F) : A \underset{1-1 onto}{⟶} G [B]$
8	5 6 7	syl2anc	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land B \subseteq C) \to (({G ↾}_{B}) \circ F) : A \underset{1-1 onto}{⟶} G [B]$
9		f1ofo	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{onto}{⟶} B$
10		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
11	9 10	syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to ran F = B$
12	11	eqimssd	$⊢ F : A \underset{1-1 onto}{⟶} B \to ran F \subseteq B$
13	12	3ad2ant1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land B \subseteq C) \to ran F \subseteq B$
14		cores	$⊢ ran F \subseteq B \to ({G ↾}_{B}) \circ F = G \circ F$
15	14	eqcomd	$⊢ ran F \subseteq B \to G \circ F = ({G ↾}_{B}) \circ F$
16	13 15	syl	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land B \subseteq C) \to G \circ F = ({G ↾}_{B}) \circ F$
17	16	f1oeq1d	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land B \subseteq C) \to ((G \circ F) : A \underset{1-1 onto}{⟶} G [B] \leftrightarrow (({G ↾}_{B}) \circ F) : A \underset{1-1 onto}{⟶} G [B])$
18	8 17	mpbird	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land B \subseteq C) \to (G \circ F) : A \underset{1-1 onto}{⟶} G [B]$