Metamath Proof Explorer

Theorem dicfnN

Description: Functionality and domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dicfn.l 
|- .<_ = ( le ` K )
dicfn.a 
|- A = ( Atoms ` K )
dicfn.h 
|- H = ( LHyp ` K )
dicfn.i 
|- I = ( ( DIsoC ` K ) ` W )
Assertion dicfnN 
|- ( ( K e. V /\ W e. H ) -> I Fn { p e. A | -. p .<_ W } )

Proof

Step Hyp Ref Expression
1 dicfn.l 
 |-  .<_ = ( le ` K )
2 dicfn.a 
 |-  A = ( Atoms ` K )
3 dicfn.h 
 |-  H = ( LHyp ` K )
4 dicfn.i 
 |-  I = ( ( DIsoC ` K ) ` W )
5 breq1 
 |-  ( p = q -> ( p .<_ W <-> q .<_ W ) )
6 5 notbid 
 |-  ( p = q -> ( -. p .<_ W <-> -. q .<_ W ) )
7 6 elrab 
 |-  ( q e. { p e. A | -. p .<_ W } <-> ( q e. A /\ -. q .<_ W ) )
8 eqid 
 |-  ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W )
9 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
10 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
11 1 2 3 8 9 10 4 dicval 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( q e. A /\ -. q .<_ W ) ) -> ( I ` q ) = { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } )
12 fvex 
 |-  ( I ` q ) e. _V
13 11 12 eqeltrrdi 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( q e. A /\ -. q .<_ W ) ) -> { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } e. _V )
14 7 13 sylan2b 
 |-  ( ( ( K e. V /\ W e. H ) /\ q e. { p e. A | -. p .<_ W } ) -> { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } e. _V )
15 14 ralrimiva 
 |-  ( ( K e. V /\ W e. H ) -> A. q e. { p e. A | -. p .<_ W } { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } e. _V )
16 eqid 
 |-  ( q e. { p e. A | -. p .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) = ( q e. { p e. A | -. p .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } )
17 16 fnmpt 
 |-  ( A. q e. { p e. A | -. p .<_ W } { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } e. _V -> ( q e. { p e. A | -. p .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) Fn { p e. A | -. p .<_ W } )
18 15 17 syl 
 |-  ( ( K e. V /\ W e. H ) -> ( q e. { p e. A | -. p .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) Fn { p e. A | -. p .<_ W } )
19 1 2 3 8 9 10 4 dicfval 
 |-  ( ( K e. V /\ W e. H ) -> I = ( q e. { p e. A | -. p .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) )
20 19 fneq1d 
 |-  ( ( K e. V /\ W e. H ) -> ( I Fn { p e. A | -. p .<_ W } <-> ( q e. { p e. A | -. p .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ u e. ( ( LTrn ` K ) ` W ) ( u ` ( ( oc ` K ) ` W ) ) = q ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) Fn { p e. A | -. p .<_ W } ) )
21 18 20 mpbird 
 |-  ( ( K e. V /\ W e. H ) -> I Fn { p e. A | -. p .<_ W } )