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 } )