Theorem fcoresf1ob

Description: A composition is bijective iff the restriction of its first component to the minimum domain is bijective and the restriction of its second component to the minimum domain is injective. (Contributed by GL and AV, 7-Oct-2024)

	Ref	Expression
Hypotheses	fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
	fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
	fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
	fcores.g	⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
	fcores.y	⊢ 𝑌 = ( 𝐺 ↾ 𝐸 )
Assertion	fcoresf1ob	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1-onto→ 𝐷 ↔ ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1-onto→ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fcores.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		fcores.e	⊢ 𝐸 = ( ran 𝐹 ∩ 𝐶 )
3		fcores.p	⊢ 𝑃 = ( ◡ 𝐹 “ 𝐶 )
4		fcores.x	⊢ 𝑋 = ( 𝐹 ↾ 𝑃 )
5		fcores.g	⊢ ( 𝜑 → 𝐺 : 𝐶 ⟶ 𝐷 )
6		fcores.y	⊢ 𝑌 = ( 𝐺 ↾ 𝐸 )
7	1 2 3 4 5 6	fcoresf1b	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ↔ ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1→ 𝐷 ) ) )
8	1 2 3 4 5 6	fcoresfob	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ↔ 𝑌 : 𝐸 –onto→ 𝐷 ) )
9	7 8	anbi12d	⊢ ( 𝜑 → ( ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ) ↔ ( ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1→ 𝐷 ) ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) ) )
10		anass	⊢ ( ( ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1→ 𝐷 ) ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) ↔ ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ ( 𝑌 : 𝐸 –1-1→ 𝐷 ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) ) )
11	9 10	bitrdi	⊢ ( 𝜑 → ( ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ) ↔ ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ ( 𝑌 : 𝐸 –1-1→ 𝐷 ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) ) ) )
12		df-f1o	⊢ ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1-onto→ 𝐷 ↔ ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1→ 𝐷 ∧ ( 𝐺 ∘ 𝐹 ) : 𝑃 –onto→ 𝐷 ) )
13		df-f1o	⊢ ( 𝑌 : 𝐸 –1-1-onto→ 𝐷 ↔ ( 𝑌 : 𝐸 –1-1→ 𝐷 ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) )
14	13	anbi2i	⊢ ( ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1-onto→ 𝐷 ) ↔ ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ ( 𝑌 : 𝐸 –1-1→ 𝐷 ∧ 𝑌 : 𝐸 –onto→ 𝐷 ) ) )
15	11 12 14	3bitr4g	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝐹 ) : 𝑃 –1-1-onto→ 𝐷 ↔ ( 𝑋 : 𝑃 –1-1→ 𝐸 ∧ 𝑌 : 𝐸 –1-1-onto→ 𝐷 ) ) )