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

Proof

Step	Hyp	Ref	Expression
1		f1of1	⊢ ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 → 𝐺 : 𝐶 –1-1→ 𝐷 )
2	1	anim1i	⊢ ( ( 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) )
3	2	3adant1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) )
4		f1ores	⊢ ( ( 𝐺 : 𝐶 –1-1→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐺 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝐺 “ 𝐵 ) )
5	3 4	syl	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐺 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝐺 “ 𝐵 ) )
6		simp1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
7		f1oco	⊢ ( ( ( 𝐺 ↾ 𝐵 ) : 𝐵 –1-1-onto→ ( 𝐺 “ 𝐵 ) ∧ 𝐹 : 𝐴 –1-1-onto→ 𝐵 ) → ( ( 𝐺 ↾ 𝐵 ) ∘ 𝐹 ) : 𝐴 –1-1-onto→ ( 𝐺 “ 𝐵 ) )
8	5 6 7	syl2anc	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐺 ↾ 𝐵 ) ∘ 𝐹 ) : 𝐴 –1-1-onto→ ( 𝐺 “ 𝐵 ) )
9		f1ofo	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –onto→ 𝐵 )
10		forn	⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ran 𝐹 = 𝐵 )
11	9 10	syl	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ran 𝐹 = 𝐵 )
12	11	eqimssd	⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ran 𝐹 ⊆ 𝐵 )
13	12	3ad2ant1	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) → ran 𝐹 ⊆ 𝐵 )
14		cores	⊢ ( ran 𝐹 ⊆ 𝐵 → ( ( 𝐺 ↾ 𝐵 ) ∘ 𝐹 ) = ( 𝐺 ∘ 𝐹 ) )
15	14	eqcomd	⊢ ( ran 𝐹 ⊆ 𝐵 → ( 𝐺 ∘ 𝐹 ) = ( ( 𝐺 ↾ 𝐵 ) ∘ 𝐹 ) )
16	13 15	syl	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐺 ∘ 𝐹 ) = ( ( 𝐺 ↾ 𝐵 ) ∘ 𝐹 ) )
17	16	f1oeq1d	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) → ( ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1-onto→ ( 𝐺 “ 𝐵 ) ↔ ( ( 𝐺 ↾ 𝐵 ) ∘ 𝐹 ) : 𝐴 –1-1-onto→ ( 𝐺 “ 𝐵 ) ) )
18	8 17	mpbird	⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐺 : 𝐶 –1-1-onto→ 𝐷 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝐺 ∘ 𝐹 ) : 𝐴 –1-1-onto→ ( 𝐺 “ 𝐵 ) )