Metamath Proof Explorer

Theorem sectpropdlem

Description: Lemma for sectpropd . (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Hypotheses sectpropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
sectpropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
Assertion sectpropdlem 
|- ( ( ph /\ P e. ( Sect ` C ) ) -> P e. ( Sect ` D ) )

Proof

Step Hyp Ref Expression
1 sectpropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 sectpropd.2 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 simpr 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> P e. ( Sect ` C ) )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
6 eqid 
 |-  ( comp ` C ) = ( comp ` C )
7 eqid 
 |-  ( Id ` C ) = ( Id ` C )
8 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
9 df-sect 
 |-  Sect = ( c e. Cat |-> ( x e. ( Base ` c ) , y e. ( Base ` c ) |-> { <. f , g >. | [. ( Hom ` c ) / h ]. ( ( f e. ( x h y ) /\ g e. ( y h x ) ) /\ ( g ( <. x , y >. ( comp ` c ) x ) f ) = ( ( Id ` c ) ` x ) ) } ) )
10 9 mptrcl 
 |-  ( P e. ( Sect ` C ) -> C e. Cat )
11 10 adantl 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> C e. Cat )
12 4 5 6 7 8 11 sectffval 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( Sect ` C ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) )
13 df-mpo 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) = { <. <. x , y >. , z >. | ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) }
14 12 13 eqtrdi 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( Sect ` C ) = { <. <. x , y >. , z >. | ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) } )
15 3 14 eleqtrd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> P e. { <. <. x , y >. , z >. | ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) } )
16 eloprab1st2nd 
 |-  ( P e. { <. <. x , y >. , z >. | ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) } -> P = <. <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. , ( 2nd ` P ) >. )
17 15 16 syl 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> P = <. <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. , ( 2nd ` P ) >. )
18 eqid 
 |-  ( comp ` D ) = ( comp ` D )
19 1 adantr 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) )
20 19 adantr 
 |-  ( ( ( ph /\ P e. ( Sect ` C ) ) /\ ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) -> ( Homf ` C ) = ( Homf ` D ) )
21 2 adantr 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( comf ` C ) = ( comf ` D ) )
22 21 adantr 
 |-  ( ( ( ph /\ P e. ( Sect ` C ) ) /\ ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) -> ( comf ` C ) = ( comf ` D ) )
23 eleq1 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( x e. ( Base ` C ) <-> ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) ) )
24 23 anbi1d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) <-> ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) )
25 oveq1 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( x ( Hom ` C ) y ) = ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) )
26 25 eleq2d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( f e. ( x ( Hom ` C ) y ) <-> f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) ) )
27 oveq2 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( y ( Hom ` C ) x ) = ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) )
28 27 eleq2d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( g e. ( y ( Hom ` C ) x ) <-> g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) )
29 26 28 anbi12d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) <-> ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) )
30 opeq1 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> <. x , y >. = <. ( 1st ` ( 1st ` P ) ) , y >. )
31 id 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> x = ( 1st ` ( 1st ` P ) ) )
32 30 31 oveq12d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( <. x , y >. ( comp ` C ) x ) = ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) )
33 32 oveqd 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) )
34 fveq2 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( ( Id ` C ) ` x ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) )
35 33 34 eqeq12d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) <-> ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) )
36 29 35 anbi12d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) <-> ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) ) )
37 36 opabbidv 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } )
38 37 eqeq2d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( z = { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } <-> z = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } ) )
39 24 38 anbi12d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) <-> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } ) ) )
40 eleq1 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( y e. ( Base ` C ) <-> ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) )
41 40 anbi2d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ y e. ( Base ` C ) ) <-> ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) ) )
42 oveq2 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) = ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) )
43 42 eleq2d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) <-> f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) ) )
44 oveq1 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) = ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) )
45 44 eleq2d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) <-> g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) )
46 43 45 anbi12d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) <-> ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) )
47 opeq2 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> <. ( 1st ` ( 1st ` P ) ) , y >. = <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. )
48 47 oveq1d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) = ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) )
49 48 oveqd 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) )
50 49 eqeq1d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) <-> ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) )
51 46 50 anbi12d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) <-> ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) ) )
52 51 opabbidv 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } )
53 52 eqeq2d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( z = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } <-> z = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } ) )
54 41 53 anbi12d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , y >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } ) <-> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) /\ z = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } ) ) )
55 eqeq1 
 |-  ( z = ( 2nd ` P ) -> ( z = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } <-> ( 2nd ` P ) = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } ) )
56 55 anbi2d 
 |-  ( z = ( 2nd ` P ) -> ( ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) /\ z = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } ) <-> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) /\ ( 2nd ` P ) = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } ) ) )
57 39 54 56 eloprabi 
 |-  ( P e. { <. <. x , y >. , z >. | ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = { <. f , g >. | ( ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) x ) ) /\ ( g ( <. x , y >. ( comp ` C ) x ) f ) = ( ( Id ` C ) ` x ) ) } ) } -> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) /\ ( 2nd ` P ) = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } ) )
58 15 57 syl 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) /\ ( 2nd ` P ) = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } ) )
59 58 simplld 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) )
60 59 adantr 
 |-  ( ( ( ph /\ P e. ( Sect ` C ) ) /\ ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) -> ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) )
61 58 simplrd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) )
62 61 adantr 
 |-  ( ( ( ph /\ P e. ( Sect ` C ) ) /\ ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) -> ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) )
63 simprl 
 |-  ( ( ( ph /\ P e. ( Sect ` C ) ) /\ ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) -> f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) )
64 simprr 
 |-  ( ( ( ph /\ P e. ( Sect ` C ) ) /\ ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) -> g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) )
65 4 5 6 18 20 22 60 62 60 63 64 comfeqval 
 |-  ( ( ( ph /\ P e. ( Sect ` C ) ) /\ ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) -> ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` D ) ( 1st ` ( 1st ` P ) ) ) f ) )
66 19 homfeqbas 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( Base ` C ) = ( Base ` D ) )
67 59 66 eleqtrd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( 1st ` ( 1st ` P ) ) e. ( Base ` D ) )
68 67 elfvexd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> D e. _V )
69 19 21 11 68 cidpropd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( Id ` C ) = ( Id ` D ) )
70 69 fveq1d 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) = ( ( Id ` D ) ` ( 1st ` ( 1st ` P ) ) ) )
71 70 adantr 
 |-  ( ( ( ph /\ P e. ( Sect ` C ) ) /\ ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) -> ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) = ( ( Id ` D ) ` ( 1st ` ( 1st ` P ) ) ) )
72 65 71 eqeq12d 
 |-  ( ( ( ph /\ P e. ( Sect ` C ) ) /\ ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) ) -> ( ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) <-> ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` D ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` D ) ` ( 1st ` ( 1st ` P ) ) ) ) )
73 72 pm5.32da 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) <-> ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` D ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` D ) ` ( 1st ` ( 1st ` P ) ) ) ) ) )
74 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
75 4 5 74 19 59 61 homfeqval 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) = ( ( 1st ` ( 1st ` P ) ) ( Hom ` D ) ( 2nd ` ( 1st ` P ) ) ) )
76 75 eleq2d 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) <-> f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` D ) ( 2nd ` ( 1st ` P ) ) ) ) )
77 4 5 74 19 61 59 homfeqval 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) = ( ( 2nd ` ( 1st ` P ) ) ( Hom ` D ) ( 1st ` ( 1st ` P ) ) ) )
78 77 eleq2d 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) <-> g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` D ) ( 1st ` ( 1st ` P ) ) ) ) )
79 76 78 anbi12d 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) <-> ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` D ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` D ) ( 1st ` ( 1st ` P ) ) ) ) ) )
80 79 anbi1d 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` D ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` D ) ` ( 1st ` ( 1st ` P ) ) ) ) <-> ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` D ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` D ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` D ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` D ) ` ( 1st ` ( 1st ` P ) ) ) ) ) )
81 73 80 bitrd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) <-> ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` D ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` D ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` D ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` D ) ` ( 1st ` ( 1st ` P ) ) ) ) ) )
82 81 opabbidv 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` D ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` D ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` D ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` D ) ` ( 1st ` ( 1st ` P ) ) ) ) } )
83 58 simprd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( 2nd ` P ) = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` C ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` C ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` C ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` C ) ` ( 1st ` ( 1st ` P ) ) ) ) } )
84 eqid 
 |-  ( Base ` D ) = ( Base ` D )
85 eqid 
 |-  ( Id ` D ) = ( Id ` D )
86 eqid 
 |-  ( Sect ` D ) = ( Sect ` D )
87 19 21 11 68 catpropd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( C e. Cat <-> D e. Cat ) )
88 11 87 mpbid 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> D e. Cat )
89 61 66 eleqtrd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( 2nd ` ( 1st ` P ) ) e. ( Base ` D ) )
90 84 74 18 85 86 88 67 89 sectfval 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( 1st ` ( 1st ` P ) ) ( Sect ` D ) ( 2nd ` ( 1st ` P ) ) ) = { <. f , g >. | ( ( f e. ( ( 1st ` ( 1st ` P ) ) ( Hom ` D ) ( 2nd ` ( 1st ` P ) ) ) /\ g e. ( ( 2nd ` ( 1st ` P ) ) ( Hom ` D ) ( 1st ` ( 1st ` P ) ) ) ) /\ ( g ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( comp ` D ) ( 1st ` ( 1st ` P ) ) ) f ) = ( ( Id ` D ) ` ( 1st ` ( 1st ` P ) ) ) ) } )
91 82 83 90 3eqtr4rd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( 1st ` ( 1st ` P ) ) ( Sect ` D ) ( 2nd ` ( 1st ` P ) ) ) = ( 2nd ` P ) )
92 sectfn 
 |-  ( D e. Cat -> ( Sect ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) )
93 88 92 syl 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( Sect ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) )
94 fnbrovb 
 |-  ( ( ( Sect ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) /\ ( ( 1st ` ( 1st ` P ) ) e. ( Base ` D ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` D ) ) ) -> ( ( ( 1st ` ( 1st ` P ) ) ( Sect ` D ) ( 2nd ` ( 1st ` P ) ) ) = ( 2nd ` P ) <-> <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( Sect ` D ) ( 2nd ` P ) ) )
95 93 67 89 94 syl12anc 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> ( ( ( 1st ` ( 1st ` P ) ) ( Sect ` D ) ( 2nd ` ( 1st ` P ) ) ) = ( 2nd ` P ) <-> <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( Sect ` D ) ( 2nd ` P ) ) )
96 91 95 mpbid 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( Sect ` D ) ( 2nd ` P ) )
97 df-br 
 |-  ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( Sect ` D ) ( 2nd ` P ) <-> <. <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. , ( 2nd ` P ) >. e. ( Sect ` D ) )
98 96 97 sylib 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> <. <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. , ( 2nd ` P ) >. e. ( Sect ` D ) )
99 17 98 eqeltrd 
 |-  ( ( ph /\ P e. ( Sect ` C ) ) -> P e. ( Sect ` D ) )