Metamath Proof Explorer

Theorem upciclem4

Description: Lemma for upcic and upeu . (Contributed by Zhi Wang, 19-Sep-2025)

Ref Expression
Hypotheses upcic.b 
|- B = ( Base ` D )
upcic.c 
|- C = ( Base ` E )
upcic.h 
|- H = ( Hom ` D )
upcic.j 
|- J = ( Hom ` E )
upcic.o 
|- O = ( comp ` E )
upcic.f 
|- ( ph -> F ( D Func E ) G )
upcic.x 
|- ( ph -> X e. B )
upcic.y 
|- ( ph -> Y e. B )
upcic.z 
|- ( ph -> Z e. C )
upcic.m 
|- ( ph -> M e. ( Z J ( F ` X ) ) )
upcic.1 
|- ( ph -> A. w e. B A. f e. ( Z J ( F ` w ) ) E! k e. ( X H w ) f = ( ( ( X G w ) ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) )
upcic.n 
|- ( ph -> N e. ( Z J ( F ` Y ) ) )
upcic.2 
|- ( ph -> A. v e. B A. g e. ( Z J ( F ` v ) ) E! l e. ( Y H v ) g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) )
Assertion upciclem4 
|- ( ph -> ( X ( ~=c ` D ) Y /\ E. r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) )

Proof

Step Hyp Ref Expression
1 upcic.b 
 |-  B = ( Base ` D )
2 upcic.c 
 |-  C = ( Base ` E )
3 upcic.h 
 |-  H = ( Hom ` D )
4 upcic.j 
 |-  J = ( Hom ` E )
5 upcic.o 
 |-  O = ( comp ` E )
6 upcic.f 
 |-  ( ph -> F ( D Func E ) G )
7 upcic.x 
 |-  ( ph -> X e. B )
8 upcic.y 
 |-  ( ph -> Y e. B )
9 upcic.z 
 |-  ( ph -> Z e. C )
10 upcic.m 
 |-  ( ph -> M e. ( Z J ( F ` X ) ) )
11 upcic.1 
 |-  ( ph -> A. w e. B A. f e. ( Z J ( F ` w ) ) E! k e. ( X H w ) f = ( ( ( X G w ) ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) )
12 upcic.n 
 |-  ( ph -> N e. ( Z J ( F ` Y ) ) )
13 upcic.2 
 |-  ( ph -> A. v e. B A. g e. ( Z J ( F ` v ) ) E! l e. ( Y H v ) g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) )
14 11 8 12 upciclem1 
 |-  ( ph -> E! p e. ( X H Y ) N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
15 reurex 
 |-  ( E! p e. ( X H Y ) N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) -> E. p e. ( X H Y ) N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
16 14 15 syl 
 |-  ( ph -> E. p e. ( X H Y ) N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
17 simpl 
 |-  ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) -> ph )
18 13 7 10 upciclem1 
 |-  ( ph -> E! q e. ( Y H X ) M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) )
19 reurex 
 |-  ( E! q e. ( Y H X ) M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) -> E. q e. ( Y H X ) M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) )
20 17 18 19 3syl 
 |-  ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) -> E. q e. ( Y H X ) M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) )
21 eqid 
 |-  ( Iso ` D ) = ( Iso ` D )
22 6 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> F ( D Func E ) G )
23 22 funcrcl2 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> D e. Cat )
24 7 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> X e. B )
25 8 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> Y e. B )
26 eqid 
 |-  ( comp ` D ) = ( comp ` D )
27 eqid 
 |-  ( Id ` D ) = ( Id ` D )
28 simplrl 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> p e. ( X H Y ) )
29 simprl 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> q e. ( Y H X ) )
30 9 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> Z e. C )
31 10 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> M e. ( Z J ( F ` X ) ) )
32 11 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> A. w e. B A. f e. ( Z J ( F ` w ) ) E! k e. ( X H w ) f = ( ( ( X G w ) ` k ) ( <. Z , ( F ` X ) >. O ( F ` w ) ) M ) )
33 simprr 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) )
34 simplrr 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
35 1 2 3 4 5 22 24 25 30 31 32 26 28 29 33 34 upciclem3 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> ( q ( <. X , Y >. ( comp ` D ) X ) p ) = ( ( Id ` D ) ` X ) )
36 12 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> N e. ( Z J ( F ` Y ) ) )
37 13 ad2antrr 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> A. v e. B A. g e. ( Z J ( F ` v ) ) E! l e. ( Y H v ) g = ( ( ( Y G v ) ` l ) ( <. Z , ( F ` Y ) >. O ( F ` v ) ) N ) )
38 1 2 3 4 5 22 25 24 30 36 37 26 29 28 34 33 upciclem3 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> ( p ( <. Y , X >. ( comp ` D ) Y ) q ) = ( ( Id ` D ) ` Y ) )
39 1 3 26 21 27 23 24 25 28 29 35 38 isisod 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> p e. ( X ( Iso ` D ) Y ) )
40 21 1 23 24 25 39 brcici 
 |-  ( ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) /\ ( q e. ( Y H X ) /\ M = ( ( ( Y G X ) ` q ) ( <. Z , ( F ` Y ) >. O ( F ` X ) ) N ) ) ) -> X ( ~=c ` D ) Y )
41 20 40 rexlimddv 
 |-  ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) -> X ( ~=c ` D ) Y )
42 16 41 rexlimddv 
 |-  ( ph -> X ( ~=c ` D ) Y )
43 20 39 rexlimddv 
 |-  ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) -> p e. ( X ( Iso ` D ) Y ) )
44 simprr 
 |-  ( ( ph /\ ( p e. ( X H Y ) /\ N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) ) -> N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
45 16 43 44 reximssdv 
 |-  ( ph -> E. p e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
46 fveq2 
 |-  ( p = r -> ( ( X G Y ) ` p ) = ( ( X G Y ) ` r ) )
47 46 oveq1d 
 |-  ( p = r -> ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
48 47 eqeq2d 
 |-  ( p = r -> ( N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) <-> N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) )
49 48 cbvrexvw 
 |-  ( E. p e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` p ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) <-> E. r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
50 45 49 sylib 
 |-  ( ph -> E. r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) )
51 42 50 jca 
 |-  ( ph -> ( X ( ~=c ` D ) Y /\ E. r e. ( X ( Iso ` D ) Y ) N = ( ( ( X G Y ) ` r ) ( <. Z , ( F ` X ) >. O ( F ` Y ) ) M ) ) )