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 𝐷 ) ↦ ⦋ ( 1^st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2^nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝐶 Nat 𝐷 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝐶 Nat 𝐷 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
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	eqtrid	⊢ ( ¬ ( 𝐶 ∈ 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 ‘ 𝑄 )

Metamath Proof Explorer

Theorem fucbas

Proof