Metamath Proof Explorer

Theorem invpropdlem

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