cofidf2

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	cofidval.i	⊢ 𝐼 = ( id_func ‘ 𝐷 )
	cofidval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	cofidval.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
	cofidval.k	⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
	cofidval.o	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘_func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
	cofidval.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	cofidf2.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
	cofidf2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	cofidf2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	cofidf2	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∧ ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) : ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) –onto→ ( 𝑋 𝐻 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cofidval.i	⊢ 𝐼 = ( id_func ‘ 𝐷 )
2		cofidval.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
3		cofidval.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
4		cofidval.k	⊢ ( 𝜑 → 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 )
5		cofidval.o	⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘_func ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐼 )
6		cofidval.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
7		cofidf2.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
8		cofidf2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9		cofidf2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10		df-br	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
11	3 10	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
12		df-br	⊢ ( 𝐾 ( 𝐸 Func 𝐷 ) 𝐿 ↔ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐸 Func 𝐷 ) )
13	4 12	sylib	⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( 𝐸 Func 𝐷 ) )
14	1 2 11 13 5 6 7 8 9	cofidf2a	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) ∧ ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) : ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) –onto→ ( 𝑋 𝐻 𝑌 ) ) )
15	3	func2nd	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐺 )
16	15	oveqd	⊢ ( 𝜑 → ( 𝑋 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) = ( 𝑋 𝐺 𝑌 ) )
17		eqidd	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )
18	3	func1st	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
19	18	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )
20	18	fveq1d	⊢ ( 𝜑 → ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) = ( 𝐹 ‘ 𝑌 ) )
21	19 20	oveq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
22	16 17 21	f1eq123d	⊢ ( 𝜑 → ( ( 𝑋 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) ↔ ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ) )
23	4	func2nd	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
24	23 19 20	oveq123d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) = ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) )
25	24 21 17	foeq123d	⊢ ( 𝜑 → ( ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) : ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) –onto→ ( 𝑋 𝐻 𝑌 ) ↔ ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) : ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) –onto→ ( 𝑋 𝐻 𝑌 ) ) )
26	22 25	anbi12d	⊢ ( 𝜑 → ( ( ( 𝑋 ( 2^nd ‘ ⟨ 𝐹 , 𝐺 ⟩ ) 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) ∧ ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) : ( ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑋 ) 𝐽 ( ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) ‘ 𝑌 ) ) –onto→ ( 𝑋 𝐻 𝑌 ) ) ↔ ( ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∧ ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) : ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) –onto→ ( 𝑋 𝐻 𝑌 ) ) ) )
27	14 26	mpbid	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1→ ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) ∧ ( ( 𝐹 ‘ 𝑋 ) 𝐿 ( 𝐹 ‘ 𝑌 ) ) : ( ( 𝐹 ‘ 𝑋 ) 𝐽 ( 𝐹 ‘ 𝑌 ) ) –onto→ ( 𝑋 𝐻 𝑌 ) ) )

Metamath Proof Explorer

Theorem cofidf2

Proof