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

Metamath Proof Explorer

Theorem 0funcALT

Description: Alternate proof of 0func . (Contributed by Zhi Wang, 7-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis 0func.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion 0funcALT ( 𝜑 → ( ∅ Func 𝐶 ) = { ⟨ ∅ , ∅ ⟩ } )

Proof

Step Hyp Ref Expression
1 0func.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 relfunc ⊢ Rel ( ∅ Func 𝐶 )
3 0ex ⊢ ∅ ∈ V
4 3 3 relsnop ⊢ Rel { ⟨ ∅ , ∅ ⟩ }
5 base0 ⊢ ∅ = ( Base ‘ ∅ )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 eqid ⊢ ( Hom ‘ ∅ ) = ( Hom ‘ ∅ )
8 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 eqid ⊢ ( Id ‘ ∅ ) = ( Id ‘ ∅ )
10 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
11 eqid ⊢ ( comp ‘ ∅ ) = ( comp ‘ ∅ )
12 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
13 0cat ⊢ ∅ ∈ Cat
14 13 a1i ⊢ ( 𝜑 → ∅ ∈ Cat )
15 5 6 7 8 9 10 11 12 14 1 isfunc ⊢ ( 𝜑 → ( 𝑓 ( ∅ Func 𝐶 ) 𝑔 ↔ ( 𝑓 : ∅ ⟶ ( Base ‘ 𝐶 ) ∧ 𝑔 ∈ X 𝑧 ∈ ( ∅ × ∅ ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ ∅ ) ‘ 𝑧 ) ) ∧ ∀ 𝑥 ∈ ∅ ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ ∅ ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ ∅ ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ∅ ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) ) )
16 f0bi ⊢ ( 𝑓 : ∅ ⟶ ( Base ‘ 𝐶 ) ↔ 𝑓 = ∅ )
17 ral0 ⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) )
18 5 funcf2lem2 ⊢ ( 𝑔 ∈ X 𝑧 ∈ ( ∅ × ∅ ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ ∅ ) ‘ 𝑧 ) ) ↔ ( 𝑔 Fn ( ∅ × ∅ ) ∧ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 𝑔 𝑦 ) : ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) ⟶ ( ( 𝑓 ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ 𝑦 ) ) ) )
19 17 18 mpbiran2 ⊢ ( 𝑔 ∈ X 𝑧 ∈ ( ∅ × ∅ ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ ∅ ) ‘ 𝑧 ) ) ↔ 𝑔 Fn ( ∅ × ∅ ) )
20 0xp ⊢ ( ∅ × ∅ ) = ∅
21 20 fneq2i ⊢ ( 𝑔 Fn ( ∅ × ∅ ) ↔ 𝑔 Fn ∅ )
22 fn0 ⊢ ( 𝑔 Fn ∅ ↔ 𝑔 = ∅ )
23 19 21 22 3bitri ⊢ ( 𝑔 ∈ X 𝑧 ∈ ( ∅ × ∅ ) ( ( ( 𝑓 ‘ ( 1st ‘ 𝑧 ) ) ( Hom ‘ 𝐶 ) ( 𝑓 ‘ ( 2nd ‘ 𝑧 ) ) ) ↑m ( ( Hom ‘ ∅ ) ‘ 𝑧 ) ) ↔ 𝑔 = ∅ )
24 ral0 ⊢ ∀ 𝑥 ∈ ∅ ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ ∅ ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐶 ) ‘ ( 𝑓 ‘ 𝑥 ) ) ∧ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑚 ∈ ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ ∅ ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ∅ ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓 ‘ 𝑥 ) , ( 𝑓 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐶 ) ( 𝑓 ‘ 𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) )
25 15 16 23 24 0funclem ⊢ ( 𝜑 → ( 𝑓 ( ∅ Func 𝐶 ) 𝑔 ↔ ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) ) )
26 brsnop ⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → ( 𝑓 { ⟨ ∅ , ∅ ⟩ } 𝑔 ↔ ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) ) )
27 3 3 26 mp2an ⊢ ( 𝑓 { ⟨ ∅ , ∅ ⟩ } 𝑔 ↔ ( 𝑓 = ∅ ∧ 𝑔 = ∅ ) )
28 25 27 bitr4di ⊢ ( 𝜑 → ( 𝑓 ( ∅ Func 𝐶 ) 𝑔 ↔ 𝑓 { ⟨ ∅ , ∅ ⟩ } 𝑔 ) )
29 2 4 28 eqbrrdiv ⊢ ( 𝜑 → ( ∅ Func 𝐶 ) = { ⟨ ∅ , ∅ ⟩ } )