Metamath Proof Explorer

Theorem cofidf1a

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

		Ref	Expression
	Hypotheses	cofidvala.i	⊢ 𝐼 = ( id_func ‘ 𝐷 )
		cofidvala.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
		cofidvala.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
		cofidvala.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐸 Func 𝐷 ) )
		cofidvala.o	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = 𝐼 )
		cofidf1a.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
	Assertion	cofidf1a	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) : 𝐵 –1-1→ 𝐶 ∧ ( 1^st ‘ 𝐺 ) : 𝐶 –onto→ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cofidvala.i	⊢ 𝐼 = ( id_func ‘ 𝐷 )
2		cofidvala.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
3		cofidvala.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 Func 𝐸 ) )
4		cofidvala.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐸 Func 𝐷 ) )
5		cofidvala.o	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = 𝐼 )
6		cofidf1a.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
7	3	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
8	2 6 7	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ 𝐶 )
9		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
10	1 2 3 4 5 9	cofidvala	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) = ( I ↾ 𝐵 ) ∧ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝐵 × 𝐵 ) ↦ ( I ↾ ( ( Hom ‘ 𝐷 ) ‘ 𝑧 ) ) ) ) )
11	10	simpld	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) = ( I ↾ 𝐵 ) )
12		fcof1	⊢ ( ( ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ 𝐶 ∧ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) = ( I ↾ 𝐵 ) ) → ( 1^st ‘ 𝐹 ) : 𝐵 –1-1→ 𝐶 )
13	8 11 12	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 –1-1→ 𝐶 )
14	4	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐸 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
15	6 2 14	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : 𝐶 ⟶ 𝐵 )
16		fcofo	⊢ ( ( ( 1^st ‘ 𝐺 ) : 𝐶 ⟶ 𝐵 ∧ ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ 𝐶 ∧ ( ( 1^st ‘ 𝐺 ) ∘ ( 1^st ‘ 𝐹 ) ) = ( I ↾ 𝐵 ) ) → ( 1^st ‘ 𝐺 ) : 𝐶 –onto→ 𝐵 )
17	15 8 11 16	syl3anc	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : 𝐶 –onto→ 𝐵 )
18	13 17	jca	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) : 𝐵 –1-1→ 𝐶 ∧ ( 1^st ‘ 𝐺 ) : 𝐶 –onto→ 𝐵 ) )