3f1oss1

Description: The composition of three bijections as bijection from the image of the domain onto the image of the range of the middle bijection. (Contributed by AV, 15-Aug-2025)

		Ref	Expression
	Assertion	3f1oss1	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ((H \circ G) \circ F^{-1}) : F [C] \underset{1-1 onto}{⟶} H [D]$

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} : B \underset{1-1 onto}{⟶} A$
2		f1of1	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} A \to F^{-1} : B \underset{1-1}{⟶} A$
3	1 2	syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} : B \underset{1-1}{⟶} A$
4	3	3ad2ant1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \to F^{-1} : B \underset{1-1}{⟶} A$
5	4	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to F^{-1} : B \underset{1-1}{⟶} A$
6		cnvimass	$⊢ {F^{-1}}^{-1} [C] \subseteq dom F^{-1}$
7		f1of	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} A \to F^{-1} : B ⟶ A$
8		fdm	$⊢ F^{-1} : B ⟶ A \to dom F^{-1} = B$
9	8	eqcomd	$⊢ F^{-1} : B ⟶ A \to B = dom F^{-1}$
10	1 7 9	3syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to B = dom F^{-1}$
11	6 10	sseqtrrid	$⊢ F : A \underset{1-1 onto}{⟶} B \to {F^{-1}}^{-1} [C] \subseteq B$
12	11	3ad2ant1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \to {F^{-1}}^{-1} [C] \subseteq B$
13	12	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to {F^{-1}}^{-1} [C] \subseteq B$
14		f1ofn	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} A \to F^{-1} Fn B$
15	1 14	syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} Fn B$
16	15	3ad2ant1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \to F^{-1} Fn B$
17	16	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to F^{-1} Fn B$
18		eqidd	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ran F^{-1} \cap C = ran F^{-1} \cap C$
19		eqidd	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to {F^{-1}}^{-1} [C] = {F^{-1}}^{-1} [C]$
20	17 18 19	rescnvimafod	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ({F^{-1} ↾}_{{F^{-1}}^{-1} [C]}) : {F^{-1}}^{-1} [C] \underset{onto}{⟶} ran F^{-1} \cap C$
21		fof	$⊢ ({F^{-1} ↾}_{{F^{-1}}^{-1} [C]}) : {F^{-1}}^{-1} [C] \underset{onto}{⟶} ran F^{-1} \cap C \to ({F^{-1} ↾}_{{F^{-1}}^{-1} [C]}) : {F^{-1}}^{-1} [C] ⟶ ran F^{-1} \cap C$
22	20 21	syl	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ({F^{-1} ↾}_{{F^{-1}}^{-1} [C]}) : {F^{-1}}^{-1} [C] ⟶ ran F^{-1} \cap C$
23		f1resf1	$⊢ (F^{-1} : B \underset{1-1}{⟶} A \land {F^{-1}}^{-1} [C] \subseteq B \land ({F^{-1} ↾}_{{F^{-1}}^{-1} [C]}) : {F^{-1}}^{-1} [C] ⟶ ran F^{-1} \cap C) \to ({F^{-1} ↾}_{{F^{-1}}^{-1} [C]}) : {F^{-1}}^{-1} [C] \underset{1-1}{⟶} ran F^{-1} \cap C$
24	5 13 22 23	syl3anc	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ({F^{-1} ↾}_{{F^{-1}}^{-1} [C]}) : {F^{-1}}^{-1} [C] \underset{1-1}{⟶} ran F^{-1} \cap C$
25		f1of1	$⊢ G : C \underset{1-1 onto}{⟶} D \to G : C \underset{1-1}{⟶} D$
26	25	3ad2ant2	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \to G : C \underset{1-1}{⟶} D$
27	26	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to G : C \underset{1-1}{⟶} D$
28		inss2	$⊢ ran F^{-1} \cap C \subseteq C$
29		f1ores	$⊢ (G : C \underset{1-1}{⟶} D \land ran F^{-1} \cap C \subseteq C) \to ({G ↾}_{(ran F^{-1} \cap C)}) : ran F^{-1} \cap C \underset{1-1 onto}{⟶} G [ran F^{-1} \cap C]$
30	27 28 29	sylancl	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ({G ↾}_{(ran F^{-1} \cap C)}) : ran F^{-1} \cap C \underset{1-1 onto}{⟶} G [ran F^{-1} \cap C]$
31		f1ofo	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} A \to F^{-1} : B \underset{onto}{⟶} A$
32		forn	$⊢ F^{-1} : B \underset{onto}{⟶} A \to ran F^{-1} = A$
33	1 31 32	3syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to ran F^{-1} = A$
34	33	3ad2ant1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \to ran F^{-1} = A$
35	34	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ran F^{-1} = A$
36	35	ineq1d	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ran F^{-1} \cap C = A \cap C$
37		incom	$⊢ A \cap C = C \cap A$
38		dfss2	$⊢ C \subseteq A \leftrightarrow C \cap A = C$
39	38	biimpi	$⊢ C \subseteq A \to C \cap A = C$
40	37 39	eqtrid	$⊢ C \subseteq A \to A \cap C = C$
41	40	ad2antrl	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to A \cap C = C$
42	36 41	eqtrd	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ran F^{-1} \cap C = C$
43	42	imaeq2d	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to G [ran F^{-1} \cap C] = G [C]$
44		f1ofn	$⊢ G : C \underset{1-1 onto}{⟶} D \to G Fn C$
45		fnima	$⊢ G Fn C \to G [C] = ran G$
46	44 45	syl	$⊢ G : C \underset{1-1 onto}{⟶} D \to G [C] = ran G$
47		f1ofo	$⊢ G : C \underset{1-1 onto}{⟶} D \to G : C \underset{onto}{⟶} D$
48		forn	$⊢ G : C \underset{onto}{⟶} D \to ran G = D$
49	47 48	syl	$⊢ G : C \underset{1-1 onto}{⟶} D \to ran G = D$
50	46 49	eqtrd	$⊢ G : C \underset{1-1 onto}{⟶} D \to G [C] = D$
51	50	3ad2ant2	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \to G [C] = D$
52	51	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to G [C] = D$
53	43 52	eqtrd	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to G [ran F^{-1} \cap C] = D$
54	53	eqcomd	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to D = G [ran F^{-1} \cap C]$
55	54	f1oeq3d	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to (({G ↾}_{(ran F^{-1} \cap C)}) : ran F^{-1} \cap C \underset{1-1 onto}{⟶} D \leftrightarrow ({G ↾}_{(ran F^{-1} \cap C)}) : ran F^{-1} \cap C \underset{1-1 onto}{⟶} G [ran F^{-1} \cap C])$
56	30 55	mpbird	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ({G ↾}_{(ran F^{-1} \cap C)}) : ran F^{-1} \cap C \underset{1-1 onto}{⟶} D$
57		f1orel	$⊢ F : A \underset{1-1 onto}{⟶} B \to Rel F$
58	57	3ad2ant1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \to Rel F$
59	58	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to Rel F$
60		dfrel2	$⊢ Rel F \leftrightarrow {F^{-1}}^{-1} = F$
61	59 60	sylib	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to {F^{-1}}^{-1} = F$
62	61	eqcomd	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to F = {F^{-1}}^{-1}$
63	62	imaeq1d	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to F [C] = {F^{-1}}^{-1} [C]$
64	63	f1oeq2d	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ((G \circ F^{-1}) : F [C] \underset{1-1 onto}{⟶} D \leftrightarrow (G \circ F^{-1}) : {F^{-1}}^{-1} [C] \underset{1-1 onto}{⟶} D)$
65	1 7	syl	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} : B ⟶ A$
66	65	3ad2ant1	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \to F^{-1} : B ⟶ A$
67	66	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to F^{-1} : B ⟶ A$
68		eqid	$⊢ ran F^{-1} \cap C = ran F^{-1} \cap C$
69		eqid	$⊢ {F^{-1}}^{-1} [C] = {F^{-1}}^{-1} [C]$
70		eqid	$⊢ {F^{-1} ↾}_{{F^{-1}}^{-1} [C]} = {F^{-1} ↾}_{{F^{-1}}^{-1} [C]}$
71		f1of	$⊢ G : C \underset{1-1 onto}{⟶} D \to G : C ⟶ D$
72	71	3ad2ant2	$⊢ (F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \to G : C ⟶ D$
73	72	adantr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to G : C ⟶ D$
74		eqid	$⊢ {G ↾}_{(ran F^{-1} \cap C)} = {G ↾}_{(ran F^{-1} \cap C)}$
75	67 68 69 70 73 74	fcoresf1ob	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ((G \circ F^{-1}) : {F^{-1}}^{-1} [C] \underset{1-1 onto}{⟶} D \leftrightarrow (({F^{-1} ↾}_{{F^{-1}}^{-1} [C]}) : {F^{-1}}^{-1} [C] \underset{1-1}{⟶} ran F^{-1} \cap C \land ({G ↾}_{(ran F^{-1} \cap C)}) : ran F^{-1} \cap C \underset{1-1 onto}{⟶} D))$
76	64 75	bitrd	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ((G \circ F^{-1}) : F [C] \underset{1-1 onto}{⟶} D \leftrightarrow (({F^{-1} ↾}_{{F^{-1}}^{-1} [C]}) : {F^{-1}}^{-1} [C] \underset{1-1}{⟶} ran F^{-1} \cap C \land ({G ↾}_{(ran F^{-1} \cap C)}) : ran F^{-1} \cap C \underset{1-1 onto}{⟶} D))$
77	24 56 76	mpbir2and	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to (G \circ F^{-1}) : F [C] \underset{1-1 onto}{⟶} D$
78		simpl3	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to H : E \underset{1-1 onto}{⟶} I$
79		simprr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to D \subseteq E$
80		f1ocoima	$⊢ ((G \circ F^{-1}) : F [C] \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I \land D \subseteq E) \to (H \circ (G \circ F^{-1})) : F [C] \underset{1-1 onto}{⟶} H [D]$
81	77 78 79 80	syl3anc	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to (H \circ (G \circ F^{-1})) : F [C] \underset{1-1 onto}{⟶} H [D]$
82		coass	$⊢ (H \circ G) \circ F^{-1} = H \circ (G \circ F^{-1})$
83		f1oeq1	$⊢ (H \circ G) \circ F^{-1} = H \circ (G \circ F^{-1}) \to (((H \circ G) \circ F^{-1}) : F [C] \underset{1-1 onto}{⟶} H [D] \leftrightarrow (H \circ (G \circ F^{-1})) : F [C] \underset{1-1 onto}{⟶} H [D])$
84	82 83	ax-mp	$⊢ ((H \circ G) \circ F^{-1}) : F [C] \underset{1-1 onto}{⟶} H [D] \leftrightarrow (H \circ (G \circ F^{-1})) : F [C] \underset{1-1 onto}{⟶} H [D]$
85	81 84	sylibr	$⊢ ((F : A \underset{1-1 onto}{⟶} B \land G : C \underset{1-1 onto}{⟶} D \land H : E \underset{1-1 onto}{⟶} I) \land (C \subseteq A \land D \subseteq E)) \to ((H \circ G) \circ F^{-1}) : F [C] \underset{1-1 onto}{⟶} H [D]$

Metamath Proof Explorer

Theorem 3f1oss1

Proof