Metamath Proof Explorer

Theorem functhinclem1

Description: Lemma for functhinc . Given the object part, there is only one possible morphism part such that the mapped morphism is in its corresponding hom-set. (Contributed by Zhi Wang, 1-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 functhinclem1.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 functhinclem1.c ⊢ 𝐶 = ( Base ‘ 𝐸 )
3 functhinclem1.h ⊢ 𝐻 = ( Hom ‘ 𝐷 )
4 functhinclem1.j ⊢ 𝐽 = ( Hom ‘ 𝐸 )
5 functhinclem1.e ⊢ ( 𝜑 → 𝐸 ∈ ThinCat )
6 functhinclem1.f ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐶 )
7 functhinclem1.k ⊢ 𝐾 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
8 functhinclem1.1 ⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
9 simpl ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) ) → 𝜑 )
10 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) ) → 𝐺 Fn ( 𝐵 × 𝐵 ) )
11 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) )
12 eqid ⊢ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) = ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) )
13 8 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) = ∅ → ( 𝑧 𝐻 𝑤 ) = ∅ ) )
14 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝐸 ∈ ThinCat )
15 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝐹 : 𝐵 ⟶ 𝐶 )
16 simprl ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑧 ∈ 𝐵 )
17 15 16 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 )
18 simprr ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → 𝑤 ∈ 𝐵 )
19 15 18 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐶 )
20 14 17 19 2 4 thincmo ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ∃* 𝑚 𝑚 ∈ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) )
21 12 13 20 mofeu ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝑧 𝐺 𝑤 ) = ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) ) )
22 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝐻 𝑦 ) = ( 𝑧 𝐻 𝑦 ) )
23 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
24 23 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
25 22 24 xpeq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝑧 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) )
26 oveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝐻 𝑦 ) = ( 𝑧 𝐻 𝑤 ) )
27 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
28 27 oveq2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) )
29 26 28 xpeq12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) )
30 ovex ⊢ ( 𝑧 𝐻 𝑤 ) ∈ V
31 ovex ⊢ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ∈ V
32 30 31 xpex ⊢ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) ∈ V
33 25 29 7 32 ovmpo ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑧 𝐾 𝑤 ) = ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) )
34 33 adantl ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 𝐾 𝑤 ) = ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) )
35 34 eqeq2d ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑧 𝐺 𝑤 ) = ( 𝑧 𝐾 𝑤 ) ↔ ( 𝑧 𝐺 𝑤 ) = ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) ) )
36 21 35 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ↔ ( 𝑧 𝐺 𝑤 ) = ( 𝑧 𝐾 𝑤 ) ) )
37 36 2ralbidva ⊢ ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) = ( 𝑧 𝐾 𝑤 ) ) )
38 simpr ⊢ ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) → 𝐺 Fn ( 𝐵 × 𝐵 ) )
39 ovex ⊢ ( 𝑥 𝐻 𝑦 ) ∈ V
40 ovex ⊢ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∈ V
41 39 40 xpex ⊢ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ∈ V
42 7 41 fnmpoi ⊢ 𝐾 Fn ( 𝐵 × 𝐵 )
43 eqfnov2 ⊢ ( ( 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ 𝐾 Fn ( 𝐵 × 𝐵 ) ) → ( 𝐺 = 𝐾 ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) = ( 𝑧 𝐾 𝑤 ) ) )
44 38 42 43 sylancl ⊢ ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) → ( 𝐺 = 𝐾 ↔ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) = ( 𝑧 𝐾 𝑤 ) ) )
45 37 44 bitr4d ⊢ ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) → ( ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ↔ 𝐺 = 𝐾 ) )
46 45 biimpa ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) → 𝐺 = 𝐾 )
47 9 10 11 46 syl21anc ⊢ ( ( 𝜑 ∧ ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) ) → 𝐺 = 𝐾 )
48 1 fvexi ⊢ 𝐵 ∈ V
49 48 48 mpoex ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ) ) ∈ V
50 7 49 eqeltri ⊢ 𝐾 ∈ V
51 eleq1 ⊢ ( 𝐺 = 𝐾 → ( 𝐺 ∈ V ↔ 𝐾 ∈ V ) )
52 50 51 mpbiri ⊢ ( 𝐺 = 𝐾 → 𝐺 ∈ V )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝐺 = 𝐾 ) → 𝐺 ∈ V )
54 fneq1 ⊢ ( 𝐺 = 𝐾 → ( 𝐺 Fn ( 𝐵 × 𝐵 ) ↔ 𝐾 Fn ( 𝐵 × 𝐵 ) ) )
55 42 54 mpbiri ⊢ ( 𝐺 = 𝐾 → 𝐺 Fn ( 𝐵 × 𝐵 ) )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝐺 = 𝐾 ) → 𝐺 Fn ( 𝐵 × 𝐵 ) )
57 simpl ⊢ ( ( 𝜑 ∧ 𝐺 = 𝐾 ) → 𝜑 )
58 simpr ⊢ ( ( 𝜑 ∧ 𝐺 = 𝐾 ) → 𝐺 = 𝐾 )
59 45 biimpar ⊢ ( ( ( 𝜑 ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ) ∧ 𝐺 = 𝐾 ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) )
60 57 56 58 59 syl21anc ⊢ ( ( 𝜑 ∧ 𝐺 = 𝐾 ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) )
61 53 56 60 3jca ⊢ ( ( 𝜑 ∧ 𝐺 = 𝐾 ) → ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) )
62 47 61 impbida ⊢ ( 𝜑 → ( ( 𝐺 ∈ V ∧ 𝐺 Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝐺 𝑤 ) : ( 𝑧 𝐻 𝑤 ) ⟶ ( ( 𝐹 ‘ 𝑧 ) 𝐽 ( 𝐹 ‘ 𝑤 ) ) ) ↔ 𝐺 = 𝐾 ) )