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	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ( 𝐻 ∘ 𝐺 ) ∘ ^◡ 𝐹 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ ( 𝐻 “ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		f1ocnv	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ^◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
2		f1of1	⊢ ( ^◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ^◡ 𝐹 : 𝐵 –1-1→ 𝐴 )
3	1 2	syl	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ^◡ 𝐹 : 𝐵 –1-1→ 𝐴 )
4	3	3ad2ant1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) → ^◡ 𝐹 : 𝐵 –1-1→ 𝐴 )
5	4	adantr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ^◡ 𝐹 : 𝐵 –1-1→ 𝐴 )
6		cnvimass	⊢ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ⊆ dom ^◡ 𝐹
7		f1of	⊢ ( ^◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ^◡ 𝐹 : 𝐵 ⟶ 𝐴 )
8		fdm	⊢ ( ^◡ 𝐹 : 𝐵 ⟶ 𝐴 → dom ^◡ 𝐹 = 𝐵 )
9	8	eqcomd	⊢ ( ^◡ 𝐹 : 𝐵 ⟶ 𝐴 → 𝐵 = dom ^◡ 𝐹 )
10	1 7 9	3syl	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐵 = dom ^◡ 𝐹 )
11	6 10	sseqtrrid	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ( ^◡ ^◡ 𝐹 “ 𝐶 ) ⊆ 𝐵 )
12	11	3ad2ant1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) → ( ^◡ ^◡ 𝐹 “ 𝐶 ) ⊆ 𝐵 )
13	12	adantr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ^◡ ^◡ 𝐹 “ 𝐶 ) ⊆ 𝐵 )
14		f1ofn	⊢ ( ^◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ^◡ 𝐹 Fn 𝐵 )
15	1 14	syl	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ^◡ 𝐹 Fn 𝐵 )
16	15	3ad2ant1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) → ^◡ 𝐹 Fn 𝐵 )
17	16	adantr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ^◡ 𝐹 Fn 𝐵 )
18		eqidd	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ran ^◡ 𝐹 ∩ 𝐶 ) = ( ran ^◡ 𝐹 ∩ 𝐶 ) )
19		eqidd	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ^◡ ^◡ 𝐹 “ 𝐶 ) = ( ^◡ ^◡ 𝐹 “ 𝐶 ) )
20	17 18 19	rescnvimafod	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) –onto→ ( ran ^◡ 𝐹 ∩ 𝐶 ) )
21		fof	⊢ ( ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) –onto→ ( ran ^◡ 𝐹 ∩ 𝐶 ) → ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) ⟶ ( ran ^◡ 𝐹 ∩ 𝐶 ) )
22	20 21	syl	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) ⟶ ( ran ^◡ 𝐹 ∩ 𝐶 ) )
23		f1resf1	⊢ ( ( ^◡ 𝐹 : 𝐵 –1-1→ 𝐴 ∧ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ⊆ 𝐵 ∧ ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) ⟶ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) → ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) –1-1→ ( ran ^◡ 𝐹 ∩ 𝐶 ) )
24	5 13 22 23	syl3anc	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) –1-1→ ( ran ^◡ 𝐹 ∩ 𝐶 ) )
25		f1of1	⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → 𝐺 : 𝐶 –1-1→ 𝐷 )
26	25	3ad2ant2	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) → 𝐺 : 𝐶 –1-1→ 𝐷 )
27	26	adantr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → 𝐺 : 𝐶 –1-1→ 𝐷 )
28		inss2	⊢ ( ran ^◡ 𝐹 ∩ 𝐶 ) ⊆ 𝐶
29		f1ores	⊢ ( ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ ( ran ^◡ 𝐹 ∩ 𝐶 ) ⊆ 𝐶 ) → ( 𝐺 ↾ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) : ( ran ^◡ 𝐹 ∩ 𝐶 ) –1-1-onto→ ( 𝐺 “ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) )
30	27 28 29	sylancl	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( 𝐺 ↾ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) : ( ran ^◡ 𝐹 ∩ 𝐶 ) –1-1-onto→ ( 𝐺 “ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) )
31		f1ofo	⊢ ( ^◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ^◡ 𝐹 : 𝐵 –onto→ 𝐴 )
32		forn	⊢ ( ^◡ 𝐹 : 𝐵 –onto→ 𝐴 → ran ^◡ 𝐹 = 𝐴 )
33	1 31 32	3syl	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ran ^◡ 𝐹 = 𝐴 )
34	33	3ad2ant1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) → ran ^◡ 𝐹 = 𝐴 )
35	34	adantr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ran ^◡ 𝐹 = 𝐴 )
36	35	ineq1d	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ran ^◡ 𝐹 ∩ 𝐶 ) = ( 𝐴 ∩ 𝐶 ) )
37		incom	⊢ ( 𝐴 ∩ 𝐶 ) = ( 𝐶 ∩ 𝐴 )
38		dfss2	⊢ ( 𝐶 ⊆ 𝐴 ↔ ( 𝐶 ∩ 𝐴 ) = 𝐶 )
39	38	biimpi	⊢ ( 𝐶 ⊆ 𝐴 → ( 𝐶 ∩ 𝐴 ) = 𝐶 )
40	37 39	eqtrid	⊢ ( 𝐶 ⊆ 𝐴 → ( 𝐴 ∩ 𝐶 ) = 𝐶 )
41	40	ad2antrl	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( 𝐴 ∩ 𝐶 ) = 𝐶 )
42	36 41	eqtrd	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ran ^◡ 𝐹 ∩ 𝐶 ) = 𝐶 )
43	42	imaeq2d	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( 𝐺 “ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) = ( 𝐺 “ 𝐶 ) )
44		f1ofn	⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → 𝐺 Fn 𝐶 )
45		fnima	⊢ ( 𝐺 Fn 𝐶 → ( 𝐺 “ 𝐶 ) = ran 𝐺 )
46	44 45	syl	⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → ( 𝐺 “ 𝐶 ) = ran 𝐺 )
47		f1ofo	⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → 𝐺 : 𝐶 –onto→ 𝐷 )
48		forn	⊢ ( 𝐺 : 𝐶 –onto→ 𝐷 → ran 𝐺 = 𝐷 )
49	47 48	syl	⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → ran 𝐺 = 𝐷 )
50	46 49	eqtrd	⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → ( 𝐺 “ 𝐶 ) = 𝐷 )
51	50	3ad2ant2	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) → ( 𝐺 “ 𝐶 ) = 𝐷 )
52	51	adantr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( 𝐺 “ 𝐶 ) = 𝐷 )
53	43 52	eqtrd	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( 𝐺 “ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) = 𝐷 )
54	53	eqcomd	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → 𝐷 = ( 𝐺 “ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) )
55	54	f1oeq3d	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ( 𝐺 ↾ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) : ( ran ^◡ 𝐹 ∩ 𝐶 ) –1-1-onto→ 𝐷 ↔ ( 𝐺 ↾ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) : ( ran ^◡ 𝐹 ∩ 𝐶 ) –1-1-onto→ ( 𝐺 “ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) ) )
56	30 55	mpbird	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( 𝐺 ↾ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) : ( ran ^◡ 𝐹 ∩ 𝐶 ) –1-1-onto→ 𝐷 )
57		f1orel	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → Rel 𝐹 )
58	57	3ad2ant1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) → Rel 𝐹 )
59	58	adantr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → Rel 𝐹 )
60		dfrel2	⊢ ( Rel 𝐹 ↔ ^◡ ^◡ 𝐹 = 𝐹 )
61	59 60	sylib	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ^◡ ^◡ 𝐹 = 𝐹 )
62	61	eqcomd	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → 𝐹 = ^◡ ^◡ 𝐹 )
63	62	imaeq1d	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( 𝐹 “ 𝐶 ) = ( ^◡ ^◡ 𝐹 “ 𝐶 ) )
64	63	f1oeq2d	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ( 𝐺 ∘ ^◡ 𝐹 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐷 ↔ ( 𝐺 ∘ ^◡ 𝐹 ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) –1-1-onto→ 𝐷 ) )
65	1 7	syl	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ^◡ 𝐹 : 𝐵 ⟶ 𝐴 )
66	65	3ad2ant1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) → ^◡ 𝐹 : 𝐵 ⟶ 𝐴 )
67	66	adantr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ^◡ 𝐹 : 𝐵 ⟶ 𝐴 )
68		eqid	⊢ ( ran ^◡ 𝐹 ∩ 𝐶 ) = ( ran ^◡ 𝐹 ∩ 𝐶 )
69		eqid	⊢ ( ^◡ ^◡ 𝐹 “ 𝐶 ) = ( ^◡ ^◡ 𝐹 “ 𝐶 )
70		eqid	⊢ ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ) = ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) )
71		f1of	⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → 𝐺 : 𝐶 ⟶ 𝐷 )
72	71	3ad2ant2	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) → 𝐺 : 𝐶 ⟶ 𝐷 )
73	72	adantr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → 𝐺 : 𝐶 ⟶ 𝐷 )
74		eqid	⊢ ( 𝐺 ↾ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) = ( 𝐺 ↾ ( ran ^◡ 𝐹 ∩ 𝐶 ) )
75	67 68 69 70 73 74	fcoresf1ob	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ( 𝐺 ∘ ^◡ 𝐹 ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) –1-1-onto→ 𝐷 ↔ ( ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) –1-1→ ( ran ^◡ 𝐹 ∩ 𝐶 ) ∧ ( 𝐺 ↾ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) : ( ran ^◡ 𝐹 ∩ 𝐶 ) –1-1-onto→ 𝐷 ) ) )
76	64 75	bitrd	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ( 𝐺 ∘ ^◡ 𝐹 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐷 ↔ ( ( ^◡ 𝐹 ↾ ( ^◡ ^◡ 𝐹 “ 𝐶 ) ) : ( ^◡ ^◡ 𝐹 “ 𝐶 ) –1-1→ ( ran ^◡ 𝐹 ∩ 𝐶 ) ∧ ( 𝐺 ↾ ( ran ^◡ 𝐹 ∩ 𝐶 ) ) : ( ran ^◡ 𝐹 ∩ 𝐶 ) –1-1-onto→ 𝐷 ) ) )
77	24 56 76	mpbir2and	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( 𝐺 ∘ ^◡ 𝐹 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐷 )
78		simpl3	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → 𝐻 : 𝐸 –1-1-onto→ 𝐼 )
79		simprr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → 𝐷 ⊆ 𝐸 )
80		f1ocoima	⊢ ( ( ( 𝐺 ∘ ^◡ 𝐹 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ∧ 𝐷 ⊆ 𝐸 ) → ( 𝐻 ∘ ( 𝐺 ∘ ^◡ 𝐹 ) ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ ( 𝐻 “ 𝐷 ) )
81	77 78 79 80	syl3anc	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( 𝐻 ∘ ( 𝐺 ∘ ^◡ 𝐹 ) ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ ( 𝐻 “ 𝐷 ) )
82		coass	⊢ ( ( 𝐻 ∘ 𝐺 ) ∘ ^◡ 𝐹 ) = ( 𝐻 ∘ ( 𝐺 ∘ ^◡ 𝐹 ) )
83		f1oeq1	⊢ ( ( ( 𝐻 ∘ 𝐺 ) ∘ ^◡ 𝐹 ) = ( 𝐻 ∘ ( 𝐺 ∘ ^◡ 𝐹 ) ) → ( ( ( 𝐻 ∘ 𝐺 ) ∘ ^◡ 𝐹 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ ( 𝐻 “ 𝐷 ) ↔ ( 𝐻 ∘ ( 𝐺 ∘ ^◡ 𝐹 ) ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ ( 𝐻 “ 𝐷 ) ) )
84	82 83	ax-mp	⊢ ( ( ( 𝐻 ∘ 𝐺 ) ∘ ^◡ 𝐹 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ ( 𝐻 “ 𝐷 ) ↔ ( 𝐻 ∘ ( 𝐺 ∘ ^◡ 𝐹 ) ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ ( 𝐻 “ 𝐷 ) )
85	81 84	sylibr	⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐻 : 𝐸 –1-1-onto→ 𝐼 ) ∧ ( 𝐶 ⊆ 𝐴 ∧ 𝐷 ⊆ 𝐸 ) ) → ( ( 𝐻 ∘ 𝐺 ) ∘ ^◡ 𝐹 ) : ( 𝐹 “ 𝐶 ) –1-1-onto→ ( 𝐻 “ 𝐷 ) )

Metamath Proof Explorer

Theorem 3f1oss1

Proof