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

Metamath Proof Explorer

Definition df-fth

Description: Function returning all the faithful functors from a category C to a category D . A faithful functor is a functor in which all the morphism maps G ( X , Y ) between objects X , Y e. C are injections. Definition 3.27(2) in Adamek p. 34. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Assertion df-fth Faith = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfth ⊢ Faith
1 vc ⊢ 𝑐
2 ccat ⊢ Cat
3 vd ⊢ 𝑑
4 vf ⊢ 𝑓
5 vg ⊢ 𝑔
6 4 cv ⊢ 𝑓
7 1 cv ⊢ 𝑐
8 cfunc ⊢ Func
9 3 cv ⊢ 𝑑
10 7 9 8 co ⊢ ( 𝑐 Func 𝑑 )
11 5 cv ⊢ 𝑔
12 6 11 10 wbr ⊢ 𝑓 ( 𝑐 Func 𝑑 ) 𝑔
13 vx ⊢ 𝑥
14 cbs ⊢ Base
15 7 14 cfv ⊢ ( Base ‘ 𝑐 )
16 vy ⊢ 𝑦
17 13 cv ⊢ 𝑥
18 16 cv ⊢ 𝑦
19 17 18 11 co ⊢ ( 𝑥 𝑔 𝑦 )
20 19 ccnv ⊢ ◡ ( 𝑥 𝑔 𝑦 )
21 20 wfun ⊢ Fun ◡ ( 𝑥 𝑔 𝑦 )
22 21 16 15 wral ⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 )
23 22 13 15 wral ⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 )
24 12 23 wa ⊢ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) )
25 24 4 5 copab ⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) }
26 1 3 2 2 25 cmpo ⊢ ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )
27 0 26 wceq ⊢ Faith = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) Fun ◡ ( 𝑥 𝑔 𝑦 ) ) } )