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

Metamath Proof Explorer

Theorem uptr2

Description: Universal property and fully faithful functor surjective on objects. (Contributed by Zhi Wang, 25-Nov-2025)

Ref Expression
Hypotheses uptr2.a 
|- A = ( Base ` C )
uptr2.b 
|- B = ( Base ` D )
uptr2.y 
|- ( ph -> Y = ( R ` X ) )
uptr2.r 
|- ( ph -> R : A -onto-> B )
uptr2.s 
|- ( ph -> R ( ( C Full D ) i^i ( C Faith D ) ) S )
uptr2.f 
|- ( ph -> ( <. K , L >. o.func <. R , S >. ) = <. F , G >. )
uptr2.x 
|- ( ph -> X e. A )
uptr2.k 
|- ( ph -> K ( D Func E ) L )
Assertion uptr2 
|- ( ph -> ( X ( <. F , G >. ( C UP E ) Z ) M <-> Y ( <. K , L >. ( D UP E ) Z ) M ) )

Proof

Step Hyp Ref Expression
1 uptr2.a 
 |-  A = ( Base ` C )
2 uptr2.b 
 |-  B = ( Base ` D )
3 uptr2.y 
 |-  ( ph -> Y = ( R ` X ) )
4 uptr2.r 
 |-  ( ph -> R : A -onto-> B )
5 uptr2.s 
 |-  ( ph -> R ( ( C Full D ) i^i ( C Faith D ) ) S )
6 uptr2.f 
 |-  ( ph -> ( <. K , L >. o.func <. R , S >. ) = <. F , G >. )
7 uptr2.x 
 |-  ( ph -> X e. A )
8 uptr2.k 
 |-  ( ph -> K ( D Func E ) L )
9 simpr 
 |-  ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> X ( <. F , G >. ( C UP E ) Z ) M )
10 eqid 
 |-  ( Base ` E ) = ( Base ` E )
11 9 10 uprcl3 
 |-  ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> Z e. ( Base ` E ) )
12 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
13 9 12 uprcl5 
 |-  ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> M e. ( Z ( Hom ` E ) ( F ` X ) ) )
14 11 13 jca 
 |-  ( ( ph /\ X ( <. F , G >. ( C UP E ) Z ) M ) -> ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) )
15 simpr 
 |-  ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> Y ( <. K , L >. ( D UP E ) Z ) M )
16 15 10 uprcl3 
 |-  ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> Z e. ( Base ` E ) )
17 15 12 uprcl5 
 |-  ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> M e. ( Z ( Hom ` E ) ( K ` Y ) ) )
18 3 fveq2d 
 |-  ( ph -> ( K ` Y ) = ( K ` ( R ` X ) ) )
19 inss1 
 |-  ( ( C Full D ) i^i ( C Faith D ) ) C_ ( C Full D )
20 fullfunc 
 |-  ( C Full D ) C_ ( C Func D )
21 19 20 sstri 
 |-  ( ( C Full D ) i^i ( C Faith D ) ) C_ ( C Func D )
22 21 ssbri 
 |-  ( R ( ( C Full D ) i^i ( C Faith D ) ) S -> R ( C Func D ) S )
23 5 22 syl 
 |-  ( ph -> R ( C Func D ) S )
24 1 23 8 6 7 cofu1a 
 |-  ( ph -> ( K ` ( R ` X ) ) = ( F ` X ) )
25 18 24 eqtrd 
 |-  ( ph -> ( K ` Y ) = ( F ` X ) )
26 25 oveq2d 
 |-  ( ph -> ( Z ( Hom ` E ) ( K ` Y ) ) = ( Z ( Hom ` E ) ( F ` X ) ) )
27 26 adantr 
 |-  ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> ( Z ( Hom ` E ) ( K ` Y ) ) = ( Z ( Hom ` E ) ( F ` X ) ) )
28 17 27 eleqtrd 
 |-  ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> M e. ( Z ( Hom ` E ) ( F ` X ) ) )
29 16 28 jca 
 |-  ( ( ph /\ Y ( <. K , L >. ( D UP E ) Z ) M ) -> ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) )
30 4 adantr 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> R : A -onto-> B )
31 fof 
 |-  ( R : A -onto-> B -> R : A --> B )
32 30 31 syl 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> R : A --> B )
33 32 ffvelcdmda 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A ) -> ( R ` x ) e. B )
34 foelrn 
 |-  ( ( R : A -onto-> B /\ y e. B ) -> E. x e. A y = ( R ` x ) )
35 30 34 sylan 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ y e. B ) -> E. x e. A y = ( R ` x ) )
36 simp3 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> y = ( R ` x ) )
37 36 fveq2d 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( K ` y ) = ( K ` ( R ` x ) ) )
38 simp1l 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ph )
39 38 23 syl 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> R ( C Func D ) S )
40 8 adantr 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> K ( D Func E ) L )
41 40 3ad2ant1 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> K ( D Func E ) L )
42 38 6 syl 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( <. K , L >. o.func <. R , S >. ) = <. F , G >. )
43 simp2 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> x e. A )
44 1 39 41 42 43 cofu1a 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( K ` ( R ` x ) ) = ( F ` x ) )
45 37 44 eqtrd 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( K ` y ) = ( F ` x ) )
46 45 oveq2d 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( Z ( Hom ` E ) ( K ` y ) ) = ( Z ( Hom ` E ) ( F ` x ) ) )
47 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
48 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
49 38 5 syl 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> R ( ( C Full D ) i^i ( C Faith D ) ) S )
50 38 7 syl 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> X e. A )
51 1 47 48 49 50 43 ffthf1o 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( X S x ) : ( X ( Hom ` C ) x ) -1-1-onto-> ( ( R ` X ) ( Hom ` D ) ( R ` x ) ) )
52 38 3 syl 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> Y = ( R ` X ) )
53 52 36 oveq12d 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( Y ( Hom ` D ) y ) = ( ( R ` X ) ( Hom ` D ) ( R ` x ) ) )
54 53 f1oeq3d 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( ( X S x ) : ( X ( Hom ` C ) x ) -1-1-onto-> ( Y ( Hom ` D ) y ) <-> ( X S x ) : ( X ( Hom ` C ) x ) -1-1-onto-> ( ( R ` X ) ( Hom ` D ) ( R ` x ) ) ) )
55 51 54 mpbird 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( X S x ) : ( X ( Hom ` C ) x ) -1-1-onto-> ( Y ( Hom ` D ) y ) )
56 f1of 
 |-  ( ( X S x ) : ( X ( Hom ` C ) x ) -1-1-onto-> ( Y ( Hom ` D ) y ) -> ( X S x ) : ( X ( Hom ` C ) x ) --> ( Y ( Hom ` D ) y ) )
57 55 56 syl 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( X S x ) : ( X ( Hom ` C ) x ) --> ( Y ( Hom ` D ) y ) )
58 57 ffvelcdmda 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ k e. ( X ( Hom ` C ) x ) ) -> ( ( X S x ) ` k ) e. ( Y ( Hom ` D ) y ) )
59 f1ofveu 
 |-  ( ( ( X S x ) : ( X ( Hom ` C ) x ) -1-1-onto-> ( Y ( Hom ` D ) y ) /\ l e. ( Y ( Hom ` D ) y ) ) -> E! k e. ( X ( Hom ` C ) x ) ( ( X S x ) ` k ) = l )
60 eqcom 
 |-  ( ( ( X S x ) ` k ) = l <-> l = ( ( X S x ) ` k ) )
61 60 reubii 
 |-  ( E! k e. ( X ( Hom ` C ) x ) ( ( X S x ) ` k ) = l <-> E! k e. ( X ( Hom ` C ) x ) l = ( ( X S x ) ` k ) )
62 59 61 sylib 
 |-  ( ( ( X S x ) : ( X ( Hom ` C ) x ) -1-1-onto-> ( Y ( Hom ` D ) y ) /\ l e. ( Y ( Hom ` D ) y ) ) -> E! k e. ( X ( Hom ` C ) x ) l = ( ( X S x ) ` k ) )
63 55 62 sylan 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ l e. ( Y ( Hom ` D ) y ) ) -> E! k e. ( X ( Hom ` C ) x ) l = ( ( X S x ) ` k ) )
64 38 25 syl 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( K ` Y ) = ( F ` X ) )
65 64 opeq2d 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> <. Z , ( K ` Y ) >. = <. Z , ( F ` X ) >. )
66 65 45 oveq12d 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( <. Z , ( K ` Y ) >. ( comp ` E ) ( K ` y ) ) = ( <. Z , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) )
67 66 adantr 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> ( <. Z , ( K ` Y ) >. ( comp ` E ) ( K ` y ) ) = ( <. Z , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) )
68 52 adantr 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> Y = ( R ` X ) )
69 simpl3 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> y = ( R ` x ) )
70 68 69 oveq12d 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> ( Y L y ) = ( ( R ` X ) L ( R ` x ) ) )
71 simprr 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> l = ( ( X S x ) ` k ) )
72 70 71 fveq12d 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> ( ( Y L y ) ` l ) = ( ( ( R ` X ) L ( R ` x ) ) ` ( ( X S x ) ` k ) ) )
73 39 adantr 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> R ( C Func D ) S )
74 41 adantr 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> K ( D Func E ) L )
75 42 adantr 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> ( <. K , L >. o.func <. R , S >. ) = <. F , G >. )
76 50 adantr 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> X e. A )
77 43 adantr 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> x e. A )
78 simprl 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> k e. ( X ( Hom ` C ) x ) )
79 1 73 74 75 76 77 47 78 cofu2a 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> ( ( ( R ` X ) L ( R ` x ) ) ` ( ( X S x ) ` k ) ) = ( ( X G x ) ` k ) )
80 72 79 eqtrd 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> ( ( Y L y ) ` l ) = ( ( X G x ) ` k ) )
81 eqidd 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> M = M )
82 67 80 81 oveq123d 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> ( ( ( Y L y ) ` l ) ( <. Z , ( K ` Y ) >. ( comp ` E ) ( K ` y ) ) M ) = ( ( ( X G x ) ` k ) ( <. Z , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) M ) )
83 82 eqeq2d 
 |-  ( ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) /\ ( k e. ( X ( Hom ` C ) x ) /\ l = ( ( X S x ) ` k ) ) ) -> ( g = ( ( ( Y L y ) ` l ) ( <. Z , ( K ` Y ) >. ( comp ` E ) ( K ` y ) ) M ) <-> g = ( ( ( X G x ) ` k ) ( <. Z , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) M ) ) )
84 58 63 83 reuxfr1dd 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( E! l e. ( Y ( Hom ` D ) y ) g = ( ( ( Y L y ) ` l ) ( <. Z , ( K ` Y ) >. ( comp ` E ) ( K ` y ) ) M ) <-> E! k e. ( X ( Hom ` C ) x ) g = ( ( ( X G x ) ` k ) ( <. Z , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) M ) ) )
85 46 84 raleqbidv 
 |-  ( ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) /\ x e. A /\ y = ( R ` x ) ) -> ( A. g e. ( Z ( Hom ` E ) ( K ` y ) ) E! l e. ( Y ( Hom ` D ) y ) g = ( ( ( Y L y ) ` l ) ( <. Z , ( K ` Y ) >. ( comp ` E ) ( K ` y ) ) M ) <-> A. g e. ( Z ( Hom ` E ) ( F ` x ) ) E! k e. ( X ( Hom ` C ) x ) g = ( ( ( X G x ) ` k ) ( <. Z , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) M ) ) )
86 33 35 85 ralxfrd2 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( A. y e. B A. g e. ( Z ( Hom ` E ) ( K ` y ) ) E! l e. ( Y ( Hom ` D ) y ) g = ( ( ( Y L y ) ` l ) ( <. Z , ( K ` Y ) >. ( comp ` E ) ( K ` y ) ) M ) <-> A. x e. A A. g e. ( Z ( Hom ` E ) ( F ` x ) ) E! k e. ( X ( Hom ` C ) x ) g = ( ( ( X G x ) ` k ) ( <. Z , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) M ) ) )
87 eqid 
 |-  ( comp ` E ) = ( comp ` E )
88 simprl 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> Z e. ( Base ` E ) )
89 3 adantr 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> Y = ( R ` X ) )
90 7 adantr 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> X e. A )
91 32 90 ffvelcdmd 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( R ` X ) e. B )
92 89 91 eqeltrd 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> Y e. B )
93 simprr 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> M e. ( Z ( Hom ` E ) ( F ` X ) ) )
94 26 adantr 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( Z ( Hom ` E ) ( K ` Y ) ) = ( Z ( Hom ` E ) ( F ` X ) ) )
95 93 94 eleqtrrd 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> M e. ( Z ( Hom ` E ) ( K ` Y ) ) )
96 2 10 48 12 87 88 40 92 95 isup 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( Y ( <. K , L >. ( D UP E ) Z ) M <-> A. y e. B A. g e. ( Z ( Hom ` E ) ( K ` y ) ) E! l e. ( Y ( Hom ` D ) y ) g = ( ( ( Y L y ) ` l ) ( <. Z , ( K ` Y ) >. ( comp ` E ) ( K ` y ) ) M ) ) )
97 23 8 cofucla 
 |-  ( ph -> ( <. K , L >. o.func <. R , S >. ) e. ( C Func E ) )
98 6 97 eqeltrrd 
 |-  ( ph -> <. F , G >. e. ( C Func E ) )
99 df-br 
 |-  ( F ( C Func E ) G <-> <. F , G >. e. ( C Func E ) )
100 98 99 sylibr 
 |-  ( ph -> F ( C Func E ) G )
101 100 adantr 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> F ( C Func E ) G )
102 1 10 47 12 87 88 101 90 93 isup 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( X ( <. F , G >. ( C UP E ) Z ) M <-> A. x e. A A. g e. ( Z ( Hom ` E ) ( F ` x ) ) E! k e. ( X ( Hom ` C ) x ) g = ( ( ( X G x ) ` k ) ( <. Z , ( F ` X ) >. ( comp ` E ) ( F ` x ) ) M ) ) )
103 86 96 102 3bitr4rd 
 |-  ( ( ph /\ ( Z e. ( Base ` E ) /\ M e. ( Z ( Hom ` E ) ( F ` X ) ) ) ) -> ( X ( <. F , G >. ( C UP E ) Z ) M <-> Y ( <. K , L >. ( D UP E ) Z ) M ) )
104 14 29 103 bibiad 
 |-  ( ph -> ( X ( <. F , G >. ( C UP E ) Z ) M <-> Y ( <. K , L >. ( D UP E ) Z ) M ) )