Metamath Proof Explorer

Theorem 0funcg2

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

Ref Expression
Hypotheses 0funcg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
0funcg.b ⊢ ( 𝜑 → ∅ = ( Base ‘ 𝐶 ) )
0funcg.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion 0funcg2 ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ( 𝐹 = ∅ ∧ 𝐺 = ∅ ) ) )

Proof

Step Hyp Ref Expression
1 0funcg.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
2 0funcg.b ⊢ ( 𝜑 → ∅ = ( Base ‘ 𝐶 ) )
3 0funcg.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
6 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
7 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
8 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
9 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
10 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
11 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
12 0catg ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ∅ = ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
13 1 2 12 syl2anc ⊢ ( 𝜑 → 𝐶 ∈ Cat )
14 4 5 6 7 8 9 10 11 13 3 isfunc ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ( 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ∧ 𝐺 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
15 2 feq2d ⊢ ( 𝜑 → ( 𝐹 : ∅ ⟶ ( Base ‘ 𝐷 ) ↔ 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ) )
16 f0bi ⊢ ( 𝐹 : ∅ ⟶ ( Base ‘ 𝐷 ) ↔ 𝐹 = ∅ )
17 15 16 bitr3di ⊢ ( 𝜑 → ( 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) ↔ 𝐹 = ∅ ) )
18 2 eqcomd ⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ∅ )
19 rzal ⊢ ( ( Base ‘ 𝐶 ) = ∅ → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
20 18 19 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) )
21 4 funcf2lem2 ⊢ ( 𝐺 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ↔ ( 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) ) )
22 21 a1i ⊢ ( 𝜑 → ( 𝐺 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ↔ ( 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 𝐺 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
23 20 22 mpbiran2d ⊢ ( 𝜑 → ( 𝐺 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ↔ 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ) )
24 2 sqxpeqd ⊢ ( 𝜑 → ( ∅ × ∅ ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
25 0xp ⊢ ( ∅ × ∅ ) = ∅
26 24 25 eqtr3di ⊢ ( 𝜑 → ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) = ∅ )
27 26 fneq2d ⊢ ( 𝜑 → ( 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ 𝐺 Fn ∅ ) )
28 fn0 ⊢ ( 𝐺 Fn ∅ ↔ 𝐺 = ∅ )
29 27 28 bitrdi ⊢ ( 𝜑 → ( 𝐺 Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ 𝐺 = ∅ ) )
30 23 29 bitrd ⊢ ( 𝜑 → ( 𝐺 ∈ X 𝑧 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ 𝐶 ) ‘ 𝑧 ) ) ↔ 𝐺 = ∅ ) )
31 rzal ⊢ ( ( Base ‘ 𝐶 ) = ∅ → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) )
32 18 31 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ( ( ( 𝑥 𝐺 𝑥 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ∀ 𝑧 ∈ ( Base ‘ 𝐶 ) ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑧 ) ( ( 𝑥 𝐺 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑧 ) ) ( ( 𝑥 𝐺 𝑦 ) ‘ 𝑚 ) ) ) )
33 14 17 30 32 0funcglem ⊢ ( 𝜑 → ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ( 𝐹 = ∅ ∧ 𝐺 = ∅ ) ) )