Metamath Proof Explorer

Theorem cic1st2nd

Description: Reconstruction of a pair of isomorphic objects in terms of its ordered pair components. (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Assertion cic1st2nd 
|- ( P e. ( ~=c ` C ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( P e. ( ~=c ` C ) -> C e. dom ~=c )
2 cicfn 
 |-  ~=c Fn Cat
3 2 fndmi 
 |-  dom ~=c = Cat
4 1 3 eleqtrdi 
 |-  ( P e. ( ~=c ` C ) -> C e. Cat )
5 relcic 
 |-  ( C e. Cat -> Rel ( ~=c ` C ) )
6 4 5 syl 
 |-  ( P e. ( ~=c ` C ) -> Rel ( ~=c ` C ) )
7 1st2nd 
 |-  ( ( Rel ( ~=c ` C ) /\ P e. ( ~=c ` C ) ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )
8 6 7 mpancom 
 |-  ( P e. ( ~=c ` C ) -> P = <. ( 1st ` P ) , ( 2nd ` P ) >. )