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

Metamath Proof Explorer

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 𝐷 )