This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dicvalrelN

Description: The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dicvalrel.h 
|- H = ( LHyp ` K )
dicvalrel.i 
|- I = ( ( DIsoC ` K ) ` W )
Assertion dicvalrelN 
|- ( ( K e. V /\ W e. H ) -> Rel ( I ` X ) )

Proof

Step Hyp Ref Expression
1 dicvalrel.h 
 |-  H = ( LHyp ` K )
2 dicvalrel.i 
 |-  I = ( ( DIsoC ` K ) ` W )
3 relopabv 
 |-  Rel { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = X ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) }
4 eqid 
 |-  ( le ` K ) = ( le ` K )
5 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
6 4 5 1 2 dicdmN 
 |-  ( ( K e. V /\ W e. H ) -> dom I = { p e. ( Atoms ` K ) | -. p ( le ` K ) W } )
7 6 eleq2d 
 |-  ( ( K e. V /\ W e. H ) -> ( X e. dom I <-> X e. { p e. ( Atoms ` K ) | -. p ( le ` K ) W } ) )
8 breq1 
 |-  ( p = X -> ( p ( le ` K ) W <-> X ( le ` K ) W ) )
9 8 notbid 
 |-  ( p = X -> ( -. p ( le ` K ) W <-> -. X ( le ` K ) W ) )
10 9 elrab 
 |-  ( X e. { p e. ( Atoms ` K ) | -. p ( le ` K ) W } <-> ( X e. ( Atoms ` K ) /\ -. X ( le ` K ) W ) )
11 7 10 bitrdi 
 |-  ( ( K e. V /\ W e. H ) -> ( X e. dom I <-> ( X e. ( Atoms ` K ) /\ -. X ( le ` K ) W ) ) )
12 11 biimpa 
 |-  ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> ( X e. ( Atoms ` K ) /\ -. X ( le ` K ) W ) )
13 eqid 
 |-  ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
14 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
15 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
16 4 5 1 13 14 15 2 dicval 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( X e. ( Atoms ` K ) /\ -. X ( le ` K ) W ) ) -> ( I ` X ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = X ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } )
17 12 16 syldan 
 |-  ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = X ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } )
18 17 releqd 
 |-  ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> ( Rel ( I ` X ) <-> Rel { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = X ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) )
19 3 18 mpbiri 
 |-  ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> Rel ( I ` X ) )
20 19 ex 
 |-  ( ( K e. V /\ W e. H ) -> ( X e. dom I -> Rel ( I ` X ) ) )
21 rel0 
 |-  Rel (/)
22 ndmfv 
 |-  ( -. X e. dom I -> ( I ` X ) = (/) )
23 22 releqd 
 |-  ( -. X e. dom I -> ( Rel ( I ` X ) <-> Rel (/) ) )
24 21 23 mpbiri 
 |-  ( -. X e. dom I -> Rel ( I ` X ) )
25 20 24 pm2.61d1 
 |-  ( ( K e. V /\ W e. H ) -> Rel ( I ` X ) )