Theorem functhinc

Description: A functor to a thin category is determined entirely by the object part. The hypothesis "functhinc.1" is related to a monotone function if preorders induced by the categories are considered ( catprs2 ), and can be obtained from funcf2 , f002 , and ralrimivva . (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Hypotheses	functhinc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	functhinc.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
	functhinc.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	functhinc.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
	functhinc.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	functhinc.e	⊢ ( 𝜑 → 𝐸 ∈ ThinCat )
	functhinc.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
	functhinc.k	⊢ 𝐾 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
	functhinc.1	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
Assertion	functhinc	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ 𝐺 = 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		functhinc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		functhinc.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
3		functhinc.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
4		functhinc.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
5		functhinc.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
6		functhinc.e	⊢ ( 𝜑 → 𝐸 ∈ ThinCat )
7		functhinc.f	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
8		functhinc.k	⊢ 𝐾 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
9		functhinc.1	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
10		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
11		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
12		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
13		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
14	6	thinccatd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
15	1 2 3 4 10 11 12 13 5 14	isfunc	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 ∈ X 𝑐 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑐 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑐 ) ) ) ↑m ( 𝐻 ‘ 𝑐 ) ) ∧ ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐷 ) 𝑐 ) 𝑓 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑓 ) ) ) ) ) )
16		3anass	⊢ ( ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐺 ∈ X 𝑐 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑐 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑐 ) ) ) ↑m ( 𝐻 ‘ 𝑐 ) ) ∧ ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐷 ) 𝑐 ) 𝑓 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑓 ) ) ) ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( 𝐺 ∈ X 𝑐 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑐 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑐 ) ) ) ↑m ( 𝐻 ‘ 𝑐 ) ) ∧ ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐷 ) 𝑐 ) 𝑓 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑓 ) ) ) ) ) )
17	15 16	bitrdi	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ( 𝐺 ∈ X 𝑐 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑐 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑐 ) ) ) ↑m ( 𝐻 ‘ 𝑐 ) ) ∧ ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐷 ) 𝑐 ) 𝑓 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑓 ) ) ) ) ) ) )
18	7 17	mpbirand	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ( 𝐺 ∈ X 𝑐 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑐 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑐 ) ) ) ↑m ( 𝐻 ‘ 𝑐 ) ) ∧ ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐷 ) 𝑐 ) 𝑓 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑓 ) ) ) ) ) )
19		funcf2lem	⊢ ( 𝐺 ∈ X 𝑐 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑐 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑐 ) ) ) ↑m ( 𝐻 ‘ 𝑐 ) ) ↔ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ( 𝑣 𝐺 𝑢 ) : ( 𝑣 𝐻 𝑢 ) ⟶ ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑢 ) ) ) )
20		simprl	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → 𝑣 ∈ 𝐵 )
21		simprr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → 𝑢 ∈ 𝐵 )
22	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
23	20 21 22	functhinclem2	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑢 ) ) = ∅ → ( 𝑣 𝐻 𝑢 ) = ∅ ) )
24	1 2 3 4 6 7 8 23	functhinclem1	⊢ ( 𝜑 → ( ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑣 ∈ 𝐵 ∀ 𝑢 ∈ 𝐵 ( 𝑣 𝐺 𝑢 ) : ( 𝑣 𝐻 𝑢 ) ⟶ ( ( 𝐹 ‘ 𝑣 ) 𝐽 ( 𝐹 ‘ 𝑢 ) ) ) ↔ 𝐺 = 𝐾 ) )
25	19 24	bitrid	⊢ ( 𝜑 → ( 𝐺 ∈ X 𝑐 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑐 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑐 ) ) ) ↑m ( 𝐻 ‘ 𝑐 ) ) ↔ 𝐺 = 𝐾 ) )
26	25	anbi1d	⊢ ( 𝜑 → ( ( 𝐺 ∈ X 𝑐 ∈ ( 𝐵 × 𝐵 ) ( ( ( 𝐹 ‘ ( 1st ‘ 𝑐 ) ) 𝐽 ( 𝐹 ‘ ( 2nd ‘ 𝑐 ) ) ) ↑m ( 𝐻 ‘ 𝑐 ) ) ∧ ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐷 ) 𝑐 ) 𝑓 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑓 ) ) ) ) ↔ ( 𝐺 = 𝐾 ∧ ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐷 ) 𝑐 ) 𝑓 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑓 ) ) ) ) ) )
27	18 26	bitrd	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ( 𝐺 = 𝐾 ∧ ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐷 ) 𝑐 ) 𝑓 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑓 ) ) ) ) ) )
28	1 2 3 4 5 6 7 8 9 10 11 12 13	functhinclem4	⊢ ( ( 𝜑 ∧ 𝐺 = 𝐾 ) → ∀ 𝑎 ∈ 𝐵 ( ( ( 𝑎 𝐺 𝑎 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑎 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑎 𝐻 𝑏 ) ∀ 𝑔 ∈ ( 𝑏 𝐻 𝑐 ) ( ( 𝑎 𝐺 𝑐 ) ‘ ( 𝑔 ( ⟨ 𝑎 , 𝑏 ⟩ ( comp ‘ 𝐷 ) 𝑐 ) 𝑓 ) ) = ( ( ( 𝑏 𝐺 𝑐 ) ‘ 𝑔 ) ( ⟨ ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑐 ) ) ( ( 𝑎 𝐺 𝑏 ) ‘ 𝑓 ) ) ) )
29	27 28	mpbiran3d	⊢ ( 𝜑 → ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ 𝐺 = 𝐾 ) )