Metamath Proof Explorer

Theorem isopropdlem

Description: Lemma for isopropd . (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 isopropdlem 
|- ( ( ph /\ P e. ( Iso ` C ) ) -> P e. ( Iso ` 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. ( Iso ` C ) ) -> P e. ( Iso ` C ) )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 eqid 
 |-  ( Inv ` C ) = ( Inv ` C )
6 df-iso 
 |-  Iso = ( c e. Cat |-> ( ( x e. _V |-> dom x ) o. ( Inv ` c ) ) )
7 6 mptrcl 
 |-  ( P e. ( Iso ` C ) -> C e. Cat )
8 7 adantl 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> C e. Cat )
9 eqid 
 |-  ( Iso ` C ) = ( Iso ` C )
10 4 5 8 9 isofval2 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( Iso ` C ) = ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> dom ( x ( Inv ` C ) y ) ) )
11 df-mpo 
 |-  ( x e. ( Base ` C ) , y e. ( Base ` C ) |-> dom ( x ( Inv ` C ) y ) ) = { <. <. x , y >. , z >. | ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = dom ( x ( Inv ` C ) y ) ) }
12 10 11 eqtrdi 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( Iso ` C ) = { <. <. x , y >. , z >. | ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = dom ( x ( Inv ` C ) y ) ) } )
13 3 12 eleqtrd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> P e. { <. <. x , y >. , z >. | ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = dom ( x ( Inv ` C ) y ) ) } )
14 eloprab1st2nd 
 |-  ( P e. { <. <. x , y >. , z >. | ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = dom ( x ( Inv ` C ) y ) ) } -> P = <. <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. , ( 2nd ` P ) >. )
15 13 14 syl 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> P = <. <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. , ( 2nd ` P ) >. )
16 1 adantr 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( Homf ` C ) = ( Homf ` D ) )
17 2 adantr 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( comf ` C ) = ( comf ` D ) )
18 16 17 invpropd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( Inv ` C ) = ( Inv ` D ) )
19 18 oveqd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) = ( ( 1st ` ( 1st ` P ) ) ( Inv ` D ) ( 2nd ` ( 1st ` P ) ) ) )
20 19 dmeqd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` D ) ( 2nd ` ( 1st ` P ) ) ) )
21 eleq1 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( x e. ( Base ` C ) <-> ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) ) )
22 21 anbi1d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) <-> ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) )
23 oveq1 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( x ( Inv ` C ) y ) = ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) y ) )
24 23 dmeqd 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> dom ( x ( Inv ` C ) y ) = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) y ) )
25 24 eqeq2d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( z = dom ( x ( Inv ` C ) y ) <-> z = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) y ) ) )
26 22 25 anbi12d 
 |-  ( x = ( 1st ` ( 1st ` P ) ) -> ( ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = dom ( x ( Inv ` C ) y ) ) <-> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) y ) ) ) )
27 eleq1 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( y e. ( Base ` C ) <-> ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) )
28 27 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 ) ) ) )
29 oveq2 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) y ) = ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) )
30 29 dmeqd 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) y ) = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) )
31 30 eqeq2d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( z = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) y ) <-> z = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) ) )
32 28 31 anbi12d 
 |-  ( y = ( 2nd ` ( 1st ` P ) ) -> ( ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) y ) ) <-> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) /\ z = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) ) ) )
33 eqeq1 
 |-  ( z = ( 2nd ` P ) -> ( z = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) <-> ( 2nd ` P ) = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) ) )
34 33 anbi2d 
 |-  ( z = ( 2nd ` P ) -> ( ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) /\ z = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) ) <-> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) /\ ( 2nd ` P ) = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) ) ) )
35 26 32 34 eloprabi 
 |-  ( P e. { <. <. x , y >. , z >. | ( ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ z = dom ( x ( Inv ` C ) y ) ) } -> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) /\ ( 2nd ` P ) = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) ) )
36 13 35 syl 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( ( ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) ) /\ ( 2nd ` P ) = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) ) )
37 36 simprd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( 2nd ` P ) = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` C ) ( 2nd ` ( 1st ` P ) ) ) )
38 eqid 
 |-  ( Base ` D ) = ( Base ` D )
39 eqid 
 |-  ( Inv ` D ) = ( Inv ` D )
40 36 simplld 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( 1st ` ( 1st ` P ) ) e. ( Base ` C ) )
41 16 homfeqbas 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( Base ` C ) = ( Base ` D ) )
42 40 41 eleqtrd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( 1st ` ( 1st ` P ) ) e. ( Base ` D ) )
43 42 elfvexd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> D e. _V )
44 16 17 8 43 catpropd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( C e. Cat <-> D e. Cat ) )
45 8 44 mpbid 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> D e. Cat )
46 36 simplrd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( 2nd ` ( 1st ` P ) ) e. ( Base ` C ) )
47 46 41 eleqtrd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( 2nd ` ( 1st ` P ) ) e. ( Base ` D ) )
48 eqid 
 |-  ( Iso ` D ) = ( Iso ` D )
49 38 39 45 42 47 48 isoval 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( ( 1st ` ( 1st ` P ) ) ( Iso ` D ) ( 2nd ` ( 1st ` P ) ) ) = dom ( ( 1st ` ( 1st ` P ) ) ( Inv ` D ) ( 2nd ` ( 1st ` P ) ) ) )
50 20 37 49 3eqtr4rd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( ( 1st ` ( 1st ` P ) ) ( Iso ` D ) ( 2nd ` ( 1st ` P ) ) ) = ( 2nd ` P ) )
51 isofn 
 |-  ( D e. Cat -> ( Iso ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) )
52 45 51 syl 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( Iso ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) )
53 fnbrovb 
 |-  ( ( ( Iso ` D ) Fn ( ( Base ` D ) X. ( Base ` D ) ) /\ ( ( 1st ` ( 1st ` P ) ) e. ( Base ` D ) /\ ( 2nd ` ( 1st ` P ) ) e. ( Base ` D ) ) ) -> ( ( ( 1st ` ( 1st ` P ) ) ( Iso ` D ) ( 2nd ` ( 1st ` P ) ) ) = ( 2nd ` P ) <-> <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( Iso ` D ) ( 2nd ` P ) ) )
54 52 42 47 53 syl12anc 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> ( ( ( 1st ` ( 1st ` P ) ) ( Iso ` D ) ( 2nd ` ( 1st ` P ) ) ) = ( 2nd ` P ) <-> <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( Iso ` D ) ( 2nd ` P ) ) )
55 50 54 mpbid 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( Iso ` D ) ( 2nd ` P ) )
56 df-br 
 |-  ( <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. ( Iso ` D ) ( 2nd ` P ) <-> <. <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. , ( 2nd ` P ) >. e. ( Iso ` D ) )
57 55 56 sylib 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> <. <. ( 1st ` ( 1st ` P ) ) , ( 2nd ` ( 1st ` P ) ) >. , ( 2nd ` P ) >. e. ( Iso ` D ) )
58 15 57 eqeltrd 
 |-  ( ( ph /\ P e. ( Iso ` C ) ) -> P e. ( Iso ` D ) )