Metamath Proof Explorer

Theorem fucbas

Description: The objects of the functor category are functors from C to D . (Contributed by Mario Carneiro, 6-Jan-2017) (Revised by Mario Carneiro, 12-Jan-2017)

Ref Expression
Hypothesis fucbas.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
Assertion fucbas ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )

Proof

Step Hyp Ref Expression
1 fucbas.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2 eqid ⊢ ( 𝐶 Func 𝐷 ) = ( 𝐶 Func 𝐷 )
3 eqid ⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
6 simpl ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝐶 ∈ Cat )
7 simpr ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝐷 ∈ Cat )
8 eqid ⊢ ( comp ‘ 𝑄 ) = ( comp ‘ 𝑄 )
9 1 2 3 4 5 6 7 8 fuccofval ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( comp ‘ 𝑄 ) = ( 𝑣 ∈ ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) , ℎ ∈ ( 𝐶 Func 𝐷 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
10 1 2 3 4 5 6 7 9 fucval ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝑄 = { ⟨ ( Base ‘ ndx ) , ( 𝐶 Func 𝐷 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝐶 Nat 𝐷 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( comp ‘ 𝑄 ) ⟩ } )
11 catstr ⊢ { ⟨ ( Base ‘ ndx ) , ( 𝐶 Func 𝐷 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝐶 Nat 𝐷 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( comp ‘ 𝑄 ) ⟩ } Struct ⟨ 1 , 1 5 ⟩
12 baseid ⊢ Base = Slot ( Base ‘ ndx )
13 snsstp1 ⊢ { ⟨ ( Base ‘ ndx ) , ( 𝐶 Func 𝐷 ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , ( 𝐶 Func 𝐷 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝐶 Nat 𝐷 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( comp ‘ 𝑄 ) ⟩ }
14 ovexd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Func 𝐷 ) ∈ V )
15 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
16 10 11 12 13 14 15 strfv3 ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( Base ‘ 𝑄 ) = ( 𝐶 Func 𝐷 ) )
17 16 eqcomd ⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 ) )
18 base0 ⊢ ∅ = ( Base ‘ ∅ )
19 funcrcl ⊢ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
20 19 con3i ⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ¬ 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
21 20 eq0rdv ⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Func 𝐷 ) = ∅ )
22 fnfuc ⊢ FuncCat Fn ( Cat × Cat )
23 22 fndmi ⊢ dom FuncCat = ( Cat × Cat )
24 23 ndmov ⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 FuncCat 𝐷 ) = ∅ )
25 1 24 syl5eq ⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → 𝑄 = ∅ )
26 25 fveq2d ⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( Base ‘ 𝑄 ) = ( Base ‘ ∅ ) )
27 18 21 26 3eqtr4a ⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 ) )
28 17 27 pm2.61i ⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )