Metamath Proof Explorer

Theorem cicrcl

Description: Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020)

Ref Expression
Assertion cicrcl 
|- ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> S e. ( Base ` C ) )

Proof

Step Hyp Ref Expression
1 cicfval 
 |-  ( C e. Cat -> ( ~=c ` C ) = ( ( Iso ` C ) supp (/) ) )
2 1 breqd 
 |-  ( C e. Cat -> ( R ( ~=c ` C ) S <-> R ( ( Iso ` C ) supp (/) ) S ) )
3 isofn 
 |-  ( C e. Cat -> ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) )
4 fvexd 
 |-  ( C e. Cat -> ( Iso ` C ) e. _V )
5 0ex 
 |-  (/) e. _V
6 5 a1i 
 |-  ( C e. Cat -> (/) e. _V )
7 df-br 
 |-  ( R ( ( Iso ` C ) supp (/) ) S <-> <. R , S >. e. ( ( Iso ` C ) supp (/) ) )
8 elsuppfng 
 |-  ( ( ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) /\ ( Iso ` C ) e. _V /\ (/) e. _V ) -> ( <. R , S >. e. ( ( Iso ` C ) supp (/) ) <-> ( <. R , S >. e. ( ( Base ` C ) X. ( Base ` C ) ) /\ ( ( Iso ` C ) ` <. R , S >. ) =/= (/) ) ) )
9 7 8 bitrid 
 |-  ( ( ( Iso ` C ) Fn ( ( Base ` C ) X. ( Base ` C ) ) /\ ( Iso ` C ) e. _V /\ (/) e. _V ) -> ( R ( ( Iso ` C ) supp (/) ) S <-> ( <. R , S >. e. ( ( Base ` C ) X. ( Base ` C ) ) /\ ( ( Iso ` C ) ` <. R , S >. ) =/= (/) ) ) )
10 3 4 6 9 syl3anc 
 |-  ( C e. Cat -> ( R ( ( Iso ` C ) supp (/) ) S <-> ( <. R , S >. e. ( ( Base ` C ) X. ( Base ` C ) ) /\ ( ( Iso ` C ) ` <. R , S >. ) =/= (/) ) ) )
11 opelxp2 
 |-  ( <. R , S >. e. ( ( Base ` C ) X. ( Base ` C ) ) -> S e. ( Base ` C ) )
12 11 adantr 
 |-  ( ( <. R , S >. e. ( ( Base ` C ) X. ( Base ` C ) ) /\ ( ( Iso ` C ) ` <. R , S >. ) =/= (/) ) -> S e. ( Base ` C ) )
13 10 12 biimtrdi 
 |-  ( C e. Cat -> ( R ( ( Iso ` C ) supp (/) ) S -> S e. ( Base ` C ) ) )
14 2 13 sylbid 
 |-  ( C e. Cat -> ( R ( ~=c ` C ) S -> S e. ( Base ` C ) ) )
15 14 imp 
 |-  ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> S e. ( Base ` C ) )