Metamath Proof Explorer

Theorem thincciso

Description: Two thin categories are isomorphic iff the induced preorders are order-isomorphic. Example 3.26(2) of Adamek p. 33. (Contributed by Zhi Wang, 16-Oct-2024)

Ref Expression
Hypotheses thincciso.c 
|- C = ( CatCat ` U )
thincciso.b 
|- B = ( Base ` C )
thincciso.r 
|- R = ( Base ` X )
thincciso.s 
|- S = ( Base ` Y )
thincciso.h 
|- H = ( Hom ` X )
thincciso.j 
|- J = ( Hom ` Y )
thincciso.u 
|- ( ph -> U e. V )
thincciso.x 
|- ( ph -> X e. B )
thincciso.y 
|- ( ph -> Y e. B )
thincciso.xt 
|- ( ph -> X e. ThinCat )
thincciso.yt 
|- ( ph -> Y e. ThinCat )
Assertion thincciso 
|- ( ph -> ( X ( ~=c ` C ) Y <-> E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) )

Proof

Step Hyp Ref Expression
1 thincciso.c 
 |-  C = ( CatCat ` U )
2 thincciso.b 
 |-  B = ( Base ` C )
3 thincciso.r 
 |-  R = ( Base ` X )
4 thincciso.s 
 |-  S = ( Base ` Y )
5 thincciso.h 
 |-  H = ( Hom ` X )
6 thincciso.j 
 |-  J = ( Hom ` Y )
7 thincciso.u 
 |-  ( ph -> U e. V )
8 thincciso.x 
 |-  ( ph -> X e. B )
9 thincciso.y 
 |-  ( ph -> Y e. B )
10 thincciso.xt 
 |-  ( ph -> X e. ThinCat )
11 thincciso.yt 
 |-  ( ph -> Y e. ThinCat )
12 eqid 
 |-  ( Iso ` C ) = ( Iso ` C )
13 1 catccat 
 |-  ( U e. V -> C e. Cat )
14 7 13 syl 
 |-  ( ph -> C e. Cat )
15 12 2 14 8 9 cic 
 |-  ( ph -> ( X ( ~=c ` C ) Y <-> E. a a e. ( X ( Iso ` C ) Y ) ) )
16 opex 
 |-  <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. _V
17 16 a1i 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. _V )
18 biimp 
 |-  ( ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) -> ( ( x H y ) = (/) -> ( ( f ` x ) J ( f ` y ) ) = (/) ) )
19 18 2ralimi 
 |-  ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) -> A. x e. R A. y e. R ( ( x H y ) = (/) -> ( ( f ` x ) J ( f ` y ) ) = (/) ) )
20 19 ad2antrl 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> A. x e. R A. y e. R ( ( x H y ) = (/) -> ( ( f ` x ) J ( f ` y ) ) = (/) ) )
21 11 adantr 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> Y e. ThinCat )
22 eqid 
 |-  ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) = ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) )
23 10 adantr 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> X e. ThinCat )
24 23 thinccd 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> X e. Cat )
25 simprr 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> f : R -1-1-onto-> S )
26 f1of 
 |-  ( f : R -1-1-onto-> S -> f : R --> S )
27 25 26 syl 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> f : R --> S )
28 biimpr 
 |-  ( ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) -> ( ( ( f ` x ) J ( f ` y ) ) = (/) -> ( x H y ) = (/) ) )
29 28 2ralimi 
 |-  ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) -> A. x e. R A. y e. R ( ( ( f ` x ) J ( f ` y ) ) = (/) -> ( x H y ) = (/) ) )
30 29 ad2antrl 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> A. x e. R A. y e. R ( ( ( f ` x ) J ( f ` y ) ) = (/) -> ( x H y ) = (/) ) )
31 3 4 5 6 24 21 27 22 30 functhinc 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> ( f ( X Func Y ) ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) <-> ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) = ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) ) )
32 22 31 mpbiri 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> f ( X Func Y ) ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) )
33 3 6 5 21 32 fullthinc 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> ( f ( X Full Y ) ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) <-> A. x e. R A. y e. R ( ( x H y ) = (/) -> ( ( f ` x ) J ( f ` y ) ) = (/) ) ) )
34 20 33 mpbird 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> f ( X Full Y ) ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) )
35 df-br 
 |-  ( f ( X Full Y ) ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) <-> <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( X Full Y ) )
36 34 35 sylib 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( X Full Y ) )
37 23 32 thincfth 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> f ( X Faith Y ) ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) )
38 df-br 
 |-  ( f ( X Faith Y ) ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) <-> <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( X Faith Y ) )
39 37 38 sylib 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( X Faith Y ) )
40 36 39 elind 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( ( X Full Y ) i^i ( X Faith Y ) ) )
41 vex 
 |-  f e. _V
42 3 fvexi 
 |-  R e. _V
43 42 42 mpoex 
 |-  ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) e. _V
44 41 43 op1st 
 |-  ( 1st ` <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. ) = f
45 f1oeq1 
 |-  ( ( 1st ` <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. ) = f -> ( ( 1st ` <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. ) : R -1-1-onto-> S <-> f : R -1-1-onto-> S ) )
46 44 45 ax-mp 
 |-  ( ( 1st ` <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. ) : R -1-1-onto-> S <-> f : R -1-1-onto-> S )
47 25 46 sylibr 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> ( 1st ` <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. ) : R -1-1-onto-> S )
48 40 47 jca 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> ( <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. ) : R -1-1-onto-> S ) )
49 1 2 3 4 7 8 9 12 catciso 
 |-  ( ph -> ( <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( X ( Iso ` C ) Y ) <-> ( <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. ) : R -1-1-onto-> S ) ) )
50 49 biimpar 
 |-  ( ( ph /\ ( <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. ) : R -1-1-onto-> S ) ) -> <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( X ( Iso ` C ) Y ) )
51 48 50 syldan 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( X ( Iso ` C ) Y ) )
52 eleq1 
 |-  ( a = <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. -> ( a e. ( X ( Iso ` C ) Y ) <-> <. f , ( z e. R , w e. R |-> ( ( z H w ) X. ( ( f ` z ) J ( f ` w ) ) ) ) >. e. ( X ( Iso ` C ) Y ) ) )
53 17 51 52 spcedv 
 |-  ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> E. a a e. ( X ( Iso ` C ) Y ) )
54 53 ex 
 |-  ( ph -> ( ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) -> E. a a e. ( X ( Iso ` C ) Y ) ) )
55 54 exlimdv 
 |-  ( ph -> ( E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) -> E. a a e. ( X ( Iso ` C ) Y ) ) )
56 fvexd 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> ( 1st ` a ) e. _V )
57 relfull 
 |-  Rel ( X Full Y )
58 1 2 3 4 7 8 9 12 catciso 
 |-  ( ph -> ( a e. ( X ( Iso ` C ) Y ) <-> ( a e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` a ) : R -1-1-onto-> S ) ) )
59 58 biimpa 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> ( a e. ( ( X Full Y ) i^i ( X Faith Y ) ) /\ ( 1st ` a ) : R -1-1-onto-> S ) )
60 59 simpld 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> a e. ( ( X Full Y ) i^i ( X Faith Y ) ) )
61 60 elin1d 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> a e. ( X Full Y ) )
62 1st2ndbr 
 |-  ( ( Rel ( X Full Y ) /\ a e. ( X Full Y ) ) -> ( 1st ` a ) ( X Full Y ) ( 2nd ` a ) )
63 57 61 62 sylancr 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> ( 1st ` a ) ( X Full Y ) ( 2nd ` a ) )
64 11 adantr 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> Y e. ThinCat )
65 fullfunc 
 |-  ( X Full Y ) C_ ( X Func Y )
66 65 ssbri 
 |-  ( ( 1st ` a ) ( X Full Y ) ( 2nd ` a ) -> ( 1st ` a ) ( X Func Y ) ( 2nd ` a ) )
67 63 66 syl 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> ( 1st ` a ) ( X Func Y ) ( 2nd ` a ) )
68 3 6 5 64 67 fullthinc 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> ( ( 1st ` a ) ( X Full Y ) ( 2nd ` a ) <-> A. x e. R A. y e. R ( ( x H y ) = (/) -> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) ) ) )
69 63 68 mpbid 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> A. x e. R A. y e. R ( ( x H y ) = (/) -> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) ) )
70 67 adantr 
 |-  ( ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) /\ ( x e. R /\ y e. R ) ) -> ( 1st ` a ) ( X Func Y ) ( 2nd ` a ) )
71 simprl 
 |-  ( ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) /\ ( x e. R /\ y e. R ) ) -> x e. R )
72 simprr 
 |-  ( ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) /\ ( x e. R /\ y e. R ) ) -> y e. R )
73 3 5 6 70 71 72 funcf2 
 |-  ( ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) /\ ( x e. R /\ y e. R ) ) -> ( x ( 2nd ` a ) y ) : ( x H y ) --> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) )
74 73 f002 
 |-  ( ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) /\ ( x e. R /\ y e. R ) ) -> ( ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) -> ( x H y ) = (/) ) )
75 74 ralrimivva 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> A. x e. R A. y e. R ( ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) -> ( x H y ) = (/) ) )
76 2ralbiim 
 |-  ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) ) <-> ( A. x e. R A. y e. R ( ( x H y ) = (/) -> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) ) /\ A. x e. R A. y e. R ( ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) -> ( x H y ) = (/) ) ) )
77 69 75 76 sylanbrc 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) ) )
78 59 simprd 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> ( 1st ` a ) : R -1-1-onto-> S )
79 77 78 jca 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) ) /\ ( 1st ` a ) : R -1-1-onto-> S ) )
80 fveq1 
 |-  ( f = ( 1st ` a ) -> ( f ` x ) = ( ( 1st ` a ) ` x ) )
81 fveq1 
 |-  ( f = ( 1st ` a ) -> ( f ` y ) = ( ( 1st ` a ) ` y ) )
82 80 81 oveq12d 
 |-  ( f = ( 1st ` a ) -> ( ( f ` x ) J ( f ` y ) ) = ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) )
83 82 eqeq1d 
 |-  ( f = ( 1st ` a ) -> ( ( ( f ` x ) J ( f ` y ) ) = (/) <-> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) ) )
84 83 bibi2d 
 |-  ( f = ( 1st ` a ) -> ( ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) <-> ( ( x H y ) = (/) <-> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) ) ) )
85 84 2ralbidv 
 |-  ( f = ( 1st ` a ) -> ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) <-> A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) ) ) )
86 f1oeq1 
 |-  ( f = ( 1st ` a ) -> ( f : R -1-1-onto-> S <-> ( 1st ` a ) : R -1-1-onto-> S ) )
87 85 86 anbi12d 
 |-  ( f = ( 1st ` a ) -> ( ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) <-> ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( ( 1st ` a ) ` x ) J ( ( 1st ` a ) ` y ) ) = (/) ) /\ ( 1st ` a ) : R -1-1-onto-> S ) ) )
88 56 79 87 spcedv 
 |-  ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) )
89 88 ex 
 |-  ( ph -> ( a e. ( X ( Iso ` C ) Y ) -> E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) )
90 89 exlimdv 
 |-  ( ph -> ( E. a a e. ( X ( Iso ` C ) Y ) -> E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) )
91 55 90 impbid 
 |-  ( ph -> ( E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) <-> E. a a e. ( X ( Iso ` C ) Y ) ) )
92 15 91 bitr4d 
 |-  ( ph -> ( X ( ~=c ` C ) Y <-> E. f ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) )