Metamath Proof Explorer

Theorem 0funcg2

Description: The functor from the empty category. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses 0funcg.c ⊢ φ → C ∈ V
0funcg.b ⊢ φ → ∅ = Base C
0funcg.d ⊢ φ → D ∈ Cat
Assertion 0funcg2 ⊢ φ → F C Func D G ↔ F = ∅ ∧ G = ∅

Proof

Step Hyp Ref Expression
1 0funcg.c ⊢ φ → C ∈ V
2 0funcg.b ⊢ φ → ∅ = Base C
3 0funcg.d ⊢ φ → D ∈ Cat
4 eqid ⊢ Base C = Base C
5 eqid ⊢ Base D = Base D
6 eqid ⊢ Hom ⁡ C = Hom ⁡ C
7 eqid ⊢ Hom ⁡ D = Hom ⁡ D
8 eqid ⊢ Id ⁡ C = Id ⁡ C
9 eqid ⊢ Id ⁡ D = Id ⁡ D
10 eqid ⊢ comp ⁡ C = comp ⁡ C
11 eqid ⊢ comp ⁡ D = comp ⁡ D
12 0catg ⊢ C ∈ V ∧ ∅ = Base C → C ∈ Cat
13 1 2 12 syl2anc ⊢ φ → C ∈ Cat
14 4 5 6 7 8 9 10 11 13 3 isfunc ⊢ φ → F C Func D G ↔ F : Base C ⟶ Base D ∧ G ∈ ⨉ z ∈ Base C × Base C F ⁡ 1 st ⁡ z Hom ⁡ D F ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ∧ ∀ x ∈ Base C x G x ⁡ Id ⁡ C ⁡ x = Id ⁡ D ⁡ F ⁡ x ∧ ∀ y ∈ Base C ∀ z ∈ Base C ∀ m ∈ x Hom ⁡ C y ∀ n ∈ y Hom ⁡ C z x G z ⁡ n x y comp ⁡ C z m = y G z ⁡ n F ⁡ x F ⁡ y comp ⁡ D F ⁡ z x G y ⁡ m
15 2 feq2d ⊢ φ → F : ∅ ⟶ Base D ↔ F : Base C ⟶ Base D
16 f0bi ⊢ F : ∅ ⟶ Base D ↔ F = ∅
17 15 16 bitr3di ⊢ φ → F : Base C ⟶ Base D ↔ F = ∅
18 2 eqcomd ⊢ φ → Base C = ∅
19 rzal ⊢ Base C = ∅ → ∀ x ∈ Base C ∀ y ∈ Base C x G y : x Hom ⁡ C y ⟶ F ⁡ x Hom ⁡ D F ⁡ y
20 18 19 syl ⊢ φ → ∀ x ∈ Base C ∀ y ∈ Base C x G y : x Hom ⁡ C y ⟶ F ⁡ x Hom ⁡ D F ⁡ y
21 4 funcf2lem2 ⊢ G ∈ ⨉ z ∈ Base C × Base C F ⁡ 1 st ⁡ z Hom ⁡ D F ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ↔ G Fn Base C × Base C ∧ ∀ x ∈ Base C ∀ y ∈ Base C x G y : x Hom ⁡ C y ⟶ F ⁡ x Hom ⁡ D F ⁡ y
22 21 a1i ⊢ φ → G ∈ ⨉ z ∈ Base C × Base C F ⁡ 1 st ⁡ z Hom ⁡ D F ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ↔ G Fn Base C × Base C ∧ ∀ x ∈ Base C ∀ y ∈ Base C x G y : x Hom ⁡ C y ⟶ F ⁡ x Hom ⁡ D F ⁡ y
23 20 22 mpbiran2d ⊢ φ → G ∈ ⨉ z ∈ Base C × Base C F ⁡ 1 st ⁡ z Hom ⁡ D F ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ↔ G Fn Base C × Base C
24 2 sqxpeqd ⊢ φ → ∅ × ∅ = Base C × Base C
25 0xp ⊢ ∅ × ∅ = ∅
26 24 25 eqtr3di ⊢ φ → Base C × Base C = ∅
27 26 fneq2d ⊢ φ → G Fn Base C × Base C ↔ G Fn ∅
28 fn0 ⊢ G Fn ∅ ↔ G = ∅
29 27 28 bitrdi ⊢ φ → G Fn Base C × Base C ↔ G = ∅
30 23 29 bitrd ⊢ φ → G ∈ ⨉ z ∈ Base C × Base C F ⁡ 1 st ⁡ z Hom ⁡ D F ⁡ 2 nd ⁡ z Hom ⁡ C ⁡ z ↔ G = ∅
31 rzal ⊢ Base C = ∅ → ∀ x ∈ Base C x G x ⁡ Id ⁡ C ⁡ x = Id ⁡ D ⁡ F ⁡ x ∧ ∀ y ∈ Base C ∀ z ∈ Base C ∀ m ∈ x Hom ⁡ C y ∀ n ∈ y Hom ⁡ C z x G z ⁡ n x y comp ⁡ C z m = y G z ⁡ n F ⁡ x F ⁡ y comp ⁡ D F ⁡ z x G y ⁡ m
32 18 31 syl ⊢ φ → ∀ x ∈ Base C x G x ⁡ Id ⁡ C ⁡ x = Id ⁡ D ⁡ F ⁡ x ∧ ∀ y ∈ Base C ∀ z ∈ Base C ∀ m ∈ x Hom ⁡ C y ∀ n ∈ y Hom ⁡ C z x G z ⁡ n x y comp ⁡ C z m = y G z ⁡ n F ⁡ x F ⁡ y comp ⁡ D F ⁡ z x G y ⁡ m
33 14 17 30 32 0funcglem ⊢ φ → F C Func D G ↔ F = ∅ ∧ G = ∅