Theorem cofidf1

Description: If " <. F , G >. is a section of <. K , L >. " in a category of small categories (in a universe), then F is injective, and K is surjective. (Contributed by Zhi Wang, 15-Nov-2025)

	Ref	Expression
Hypotheses	cofidval.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
	cofidval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	cofidval.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
	cofidval.k	⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
	cofidval.o	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
	cofidf1.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
Assertion	cofidf1	⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐾 : 𝐶 –onto→ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cofidval.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
2		cofidval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
3		cofidval.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
4		cofidval.k	⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
5		cofidval.o	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
6		cofidf1.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
7	2 6 3	funcf1	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
8		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9	1 2 3 4 5 8	cofidval	⊢ ( 𝜑 → ( ( 𝐾 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝐹 ‘ 𝑦 ) ) ∘ ( 𝑥 𝐺 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) )
10	9	simpld	⊢ ( 𝜑 → ( 𝐾 ∘ 𝐹 ) = ( I ↾ 𝐵 ) )
11		fcof1	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( 𝐾 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ) → 𝐹 : 𝐵 –1-1→ 𝐶 )
12	7 10 11	syl2anc	⊢ ( 𝜑 → 𝐹 : 𝐵 –1-1→ 𝐶 )
13	6 2 4	funcf1	⊢ ( 𝜑 → 𝐾 : 𝐶 ⟶ 𝐵 )
14		fcofo	⊢ ( ( 𝐾 : 𝐶 ⟶ 𝐵 ∧ 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( 𝐾 ∘ 𝐹 ) = ( I ↾ 𝐵 ) ) → 𝐾 : 𝐶 –onto→ 𝐵 )
15	13 7 10 14	syl3anc	⊢ ( 𝜑 → 𝐾 : 𝐶 –onto→ 𝐵 )
16	12 15	jca	⊢ ( 𝜑 → ( 𝐹 : 𝐵 –1-1→ 𝐶 ∧ 𝐾 : 𝐶 –onto→ 𝐵 ) )