This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ 𝐵 ) )