Theorem fullfunc

Description: A full functor is a functor. (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Assertion	fullfunc	⊢ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝑐 = 𝐶 → ( 𝑐 Full 𝑑 ) = ( 𝐶 Full 𝑑 ) )
2		oveq1	⊢ ( 𝑐 = 𝐶 → ( 𝑐 Func 𝑑 ) = ( 𝐶 Func 𝑑 ) )
3	1 2	sseq12d	⊢ ( 𝑐 = 𝐶 → ( ( 𝑐 Full 𝑑 ) ⊆ ( 𝑐 Func 𝑑 ) ↔ ( 𝐶 Full 𝑑 ) ⊆ ( 𝐶 Func 𝑑 ) ) )
4		oveq2	⊢ ( 𝑑 = 𝐷 → ( 𝐶 Full 𝑑 ) = ( 𝐶 Full 𝐷 ) )
5		oveq2	⊢ ( 𝑑 = 𝐷 → ( 𝐶 Func 𝑑 ) = ( 𝐶 Func 𝐷 ) )
6	4 5	sseq12d	⊢ ( 𝑑 = 𝐷 → ( ( 𝐶 Full 𝑑 ) ⊆ ( 𝐶 Func 𝑑 ) ↔ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 ) ) )
7		ovex	⊢ ( 𝑐 Func 𝑑 ) ∈ V
8		simpl	⊢ ( ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) → 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 )
9	8	ssopab2i	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } ⊆ { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 }
10		opabss	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 } ⊆ ( 𝑐 Func 𝑑 )
11	9 10	sstri	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } ⊆ ( 𝑐 Func 𝑑 )
12	7 11	ssexi	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V
13		df-full	⊢ Full = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
14	13	ovmpt4g	⊢ ( ( 𝑐 ∈ Cat ∧ 𝑑 ∈ Cat ∧ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } ∈ V ) → ( 𝑐 Full 𝑑 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
15	12 14	mp3an3	⊢ ( ( 𝑐 ∈ Cat ∧ 𝑑 ∈ Cat ) → ( 𝑐 Full 𝑑 ) = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( 𝑓 ( 𝑐 Func 𝑑 ) 𝑔 ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑐 ) ∀ 𝑦 ∈ ( Base ‘ 𝑐 ) ran ( 𝑥 𝑔 𝑦 ) = ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝑑 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
16	15 11	eqsstrdi	⊢ ( ( 𝑐 ∈ Cat ∧ 𝑑 ∈ Cat ) → ( 𝑐 Full 𝑑 ) ⊆ ( 𝑐 Func 𝑑 ) )
17	3 6 16	vtocl2ga	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 ) )
18	13	mpondm0	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Full 𝐷 ) = ∅ )
19		0ss	⊢ ∅ ⊆ ( 𝐶 Func 𝐷 )
20	18 19	eqsstrdi	⊢ ( ¬ ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 ) )
21	17 20	pm2.61i	⊢ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )