cofidf2a

Description: If " F is a section of G " in a category of small categories (in a universe), then the morphism part of F is injective, and the morphism part of G is surjective in the image of F . (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 𝐹 ) = 𝐼 )
	cofidvala.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	cofidf2a.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
	cofidf2a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cofidf2a.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	cofidf2a	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∧ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 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		cofidvala.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
7		cofidf2a.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
8		cofidf2a.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9		cofidf2a.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10	3	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐹 ) )
11	2 6 7 10 8 9	funcf2	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )
12	5	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) = ( 2^nd ‘ 𝐼 ) )
13	12	oveqd	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑌 ) = ( 𝑋 ( 2^nd ‘ 𝐼 ) 𝑌 ) )
14	2 3 4 8 9	cofu2nd	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑌 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) )
15	10	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
16	1 2 15 6 8 9	idfu2nd	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐼 ) 𝑌 ) = ( I ↾ ( 𝑋 𝐻 𝑌 ) ) )
17	13 14 16	3eqtr3d	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) = ( I ↾ ( 𝑋 𝐻 𝑌 ) ) )
18		fcof1	⊢ ( ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∧ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) = ( I ↾ ( 𝑋 𝐻 𝑌 ) ) ) → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )
19	11 17 18	syl2anc	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) )
20	1 2 8 3 4 5	cofid1a	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) = 𝑋 )
21	1 2 9 3 4 5	cofid1a	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) = 𝑌 )
22	20 21	oveq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) 𝐻 ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ) = ( 𝑋 𝐻 𝑌 ) )
23		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
24	4	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐸 Func 𝐷 ) ( 2^nd ‘ 𝐺 ) )
25	2 23 10	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : 𝐵 ⟶ ( Base ‘ 𝐸 ) )
26	25 8	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐸 ) )
27	25 9	ffvelcdmd	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ∈ ( Base ‘ 𝐸 ) )
28	23 7 6 24 26 27	funcf2	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ⟶ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ) 𝐻 ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ) )
29	22 28	feq3dd	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ⟶ ( 𝑋 𝐻 𝑌 ) )
30		fcofo	⊢ ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ⟶ ( 𝑋 𝐻 𝑌 ) ∧ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∧ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∘ ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) ) = ( I ↾ ( 𝑋 𝐻 𝑌 ) ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) –onto→ ( 𝑋 𝐻 𝑌 ) )
31	29 11 17 30	syl3anc	⊢ ( 𝜑 → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) –onto→ ( 𝑋 𝐻 𝑌 ) )
32	19 31	jca	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ 𝐹 ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) ∧ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ 𝐹 ) ‘ 𝑌 ) ) –onto→ ( 𝑋 𝐻 𝑌 ) ) )

Metamath Proof Explorer

Theorem cofidf2a

Proof