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 
|- B = ( Base ` D )
functhinclem1.c 
|- C = ( Base ` E )
functhinclem1.h 
|- H = ( Hom ` D )
functhinclem1.j 
|- J = ( Hom ` E )
functhinclem1.e 
|- ( ph -> E e. ThinCat )
functhinclem1.f 
|- ( ph -> F : B --> C )
functhinclem1.k 
|- K = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) )
functhinclem1.1 
|- ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
Assertion functhinclem1 
|- ( ph -> ( ( G e. _V /\ G Fn ( B X. B ) /\ A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) ) <-> G = K ) )

Proof

Step Hyp Ref Expression
1 functhinclem1.b 
 |-  B = ( Base ` D )
2 functhinclem1.c 
 |-  C = ( Base ` E )
3 functhinclem1.h 
 |-  H = ( Hom ` D )
4 functhinclem1.j 
 |-  J = ( Hom ` E )
5 functhinclem1.e 
 |-  ( ph -> E e. ThinCat )
6 functhinclem1.f 
 |-  ( ph -> F : B --> C )
7 functhinclem1.k 
 |-  K = ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) )
8 functhinclem1.1 
 |-  ( ( ph /\ ( z e. B /\ w e. B ) ) -> ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
9 simpl 
 |-  ( ( ph /\ ( G e. _V /\ G Fn ( B X. B ) /\ A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) ) ) -> ph )
10 simpr2 
 |-  ( ( ph /\ ( G e. _V /\ G Fn ( B X. B ) /\ A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) ) ) -> G Fn ( B X. B ) )
11 simpr3 
 |-  ( ( ph /\ ( G e. _V /\ G Fn ( B X. B ) /\ A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) ) ) -> A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) )
12 eqid 
 |-  ( ( z H w ) X. ( ( F ` z ) J ( F ` w ) ) ) = ( ( z H w ) X. ( ( F ` z ) J ( F ` w ) ) )
13 8 adantlr 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> ( ( ( F ` z ) J ( F ` w ) ) = (/) -> ( z H w ) = (/) ) )
14 5 ad2antrr 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> E e. ThinCat )
15 6 ad2antrr 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> F : B --> C )
16 simprl 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> z e. B )
17 15 16 ffvelrnd 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> ( F ` z ) e. C )
18 simprr 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> w e. B )
19 15 18 ffvelrnd 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> ( F ` w ) e. C )
20 14 17 19 2 4 thincmo 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> E* m m e. ( ( F ` z ) J ( F ` w ) ) )
21 12 13 20 mofeu 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> ( ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) <-> ( z G w ) = ( ( z H w ) X. ( ( F ` z ) J ( F ` w ) ) ) ) )
22 oveq1 
 |-  ( x = z -> ( x H y ) = ( z H y ) )
23 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
24 23 oveq1d 
 |-  ( x = z -> ( ( F ` x ) J ( F ` y ) ) = ( ( F ` z ) J ( F ` y ) ) )
25 22 24 xpeq12d 
 |-  ( x = z -> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) = ( ( z H y ) X. ( ( F ` z ) J ( F ` y ) ) ) )
26 oveq2 
 |-  ( y = w -> ( z H y ) = ( z H w ) )
27 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
28 27 oveq2d 
 |-  ( y = w -> ( ( F ` z ) J ( F ` y ) ) = ( ( F ` z ) J ( F ` w ) ) )
29 26 28 xpeq12d 
 |-  ( y = w -> ( ( z H y ) X. ( ( F ` z ) J ( F ` y ) ) ) = ( ( z H w ) X. ( ( F ` z ) J ( F ` w ) ) ) )
30 ovex 
 |-  ( z H w ) e. _V
31 ovex 
 |-  ( ( F ` z ) J ( F ` w ) ) e. _V
32 30 31 xpex 
 |-  ( ( z H w ) X. ( ( F ` z ) J ( F ` w ) ) ) e. _V
33 25 29 7 32 ovmpo 
 |-  ( ( z e. B /\ w e. B ) -> ( z K w ) = ( ( z H w ) X. ( ( F ` z ) J ( F ` w ) ) ) )
34 33 adantl 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> ( z K w ) = ( ( z H w ) X. ( ( F ` z ) J ( F ` w ) ) ) )
35 34 eqeq2d 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> ( ( z G w ) = ( z K w ) <-> ( z G w ) = ( ( z H w ) X. ( ( F ` z ) J ( F ` w ) ) ) ) )
36 21 35 bitr4d 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ ( z e. B /\ w e. B ) ) -> ( ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) <-> ( z G w ) = ( z K w ) ) )
37 36 2ralbidva 
 |-  ( ( ph /\ G Fn ( B X. B ) ) -> ( A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) <-> A. z e. B A. w e. B ( z G w ) = ( z K w ) ) )
38 simpr 
 |-  ( ( ph /\ G Fn ( B X. B ) ) -> G Fn ( B X. B ) )
39 ovex 
 |-  ( x H y ) e. _V
40 ovex 
 |-  ( ( F ` x ) J ( F ` y ) ) e. _V
41 39 40 xpex 
 |-  ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) e. _V
42 7 41 fnmpoi 
 |-  K Fn ( B X. B )
43 eqfnov2 
 |-  ( ( G Fn ( B X. B ) /\ K Fn ( B X. B ) ) -> ( G = K <-> A. z e. B A. w e. B ( z G w ) = ( z K w ) ) )
44 38 42 43 sylancl 
 |-  ( ( ph /\ G Fn ( B X. B ) ) -> ( G = K <-> A. z e. B A. w e. B ( z G w ) = ( z K w ) ) )
45 37 44 bitr4d 
 |-  ( ( ph /\ G Fn ( B X. B ) ) -> ( A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) <-> G = K ) )
46 45 biimpa 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) ) -> G = K )
47 9 10 11 46 syl21anc 
 |-  ( ( ph /\ ( G e. _V /\ G Fn ( B X. B ) /\ A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) ) ) -> G = K )
48 1 fvexi 
 |-  B e. _V
49 48 48 mpoex 
 |-  ( x e. B , y e. B |-> ( ( x H y ) X. ( ( F ` x ) J ( F ` y ) ) ) ) e. _V
50 7 49 eqeltri 
 |-  K e. _V
51 eleq1 
 |-  ( G = K -> ( G e. _V <-> K e. _V ) )
52 50 51 mpbiri 
 |-  ( G = K -> G e. _V )
53 52 adantl 
 |-  ( ( ph /\ G = K ) -> G e. _V )
54 fneq1 
 |-  ( G = K -> ( G Fn ( B X. B ) <-> K Fn ( B X. B ) ) )
55 42 54 mpbiri 
 |-  ( G = K -> G Fn ( B X. B ) )
56 55 adantl 
 |-  ( ( ph /\ G = K ) -> G Fn ( B X. B ) )
57 simpl 
 |-  ( ( ph /\ G = K ) -> ph )
58 simpr 
 |-  ( ( ph /\ G = K ) -> G = K )
59 45 biimpar 
 |-  ( ( ( ph /\ G Fn ( B X. B ) ) /\ G = K ) -> A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) )
60 57 56 58 59 syl21anc 
 |-  ( ( ph /\ G = K ) -> A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) )
61 53 56 60 3jca 
 |-  ( ( ph /\ G = K ) -> ( G e. _V /\ G Fn ( B X. B ) /\ A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) ) )
62 47 61 impbida 
 |-  ( ph -> ( ( G e. _V /\ G Fn ( B X. B ) /\ A. z e. B A. w e. B ( z G w ) : ( z H w ) --> ( ( F ` z ) J ( F ` w ) ) ) <-> G = K ) )