Metamath Proof Explorer

Theorem dicval

Description: The partial isomorphism C for a lattice K . (Contributed by NM, 15-Dec-2013) (Revised by Mario Carneiro, 22-Sep-2015)

Ref Expression
Hypotheses dicval.l 
|- .<_ = ( le ` K )
dicval.a 
|- A = ( Atoms ` K )
dicval.h 
|- H = ( LHyp ` K )
dicval.p 
|- P = ( ( oc ` K ) ` W )
dicval.t 
|- T = ( ( LTrn ` K ) ` W )
dicval.e 
|- E = ( ( TEndo ` K ) ` W )
dicval.i 
|- I = ( ( DIsoC ` K ) ` W )
Assertion dicval 
|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } )

Proof

Step Hyp Ref Expression
1 dicval.l 
 |-  .<_ = ( le ` K )
2 dicval.a 
 |-  A = ( Atoms ` K )
3 dicval.h 
 |-  H = ( LHyp ` K )
4 dicval.p 
 |-  P = ( ( oc ` K ) ` W )
5 dicval.t 
 |-  T = ( ( LTrn ` K ) ` W )
6 dicval.e 
 |-  E = ( ( TEndo ` K ) ` W )
7 dicval.i 
 |-  I = ( ( DIsoC ` K ) ` W )
8 1 2 3 4 5 6 7 dicfval 
 |-  ( ( K e. V /\ W e. H ) -> I = ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) )
9 8 adantr 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> I = ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) )
10 9 fveq1d 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = ( ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) ` Q ) )
11 simpr 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( Q e. A /\ -. Q .<_ W ) )
12 breq1 
 |-  ( r = Q -> ( r .<_ W <-> Q .<_ W ) )
13 12 notbid 
 |-  ( r = Q -> ( -. r .<_ W <-> -. Q .<_ W ) )
14 13 elrab 
 |-  ( Q e. { r e. A | -. r .<_ W } <-> ( Q e. A /\ -. Q .<_ W ) )
15 11 14 sylibr 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> Q e. { r e. A | -. r .<_ W } )
16 eqeq2 
 |-  ( q = Q -> ( ( g ` P ) = q <-> ( g ` P ) = Q ) )
17 16 riotabidv 
 |-  ( q = Q -> ( iota_ g e. T ( g ` P ) = q ) = ( iota_ g e. T ( g ` P ) = Q ) )
18 17 fveq2d 
 |-  ( q = Q -> ( s ` ( iota_ g e. T ( g ` P ) = q ) ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) )
19 18 eqeq2d 
 |-  ( q = Q -> ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) <-> f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) ) )
20 19 anbi1d 
 |-  ( q = Q -> ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) <-> ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) ) )
21 20 opabbidv 
 |-  ( q = Q -> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } = { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } )
22 eqid 
 |-  ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) = ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } )
23 6 fvexi 
 |-  E e. _V
24 23 uniex 
 |-  U. E e. _V
25 24 rnex 
 |-  ran U. E e. _V
26 25 uniex 
 |-  U. ran U. E e. _V
27 26 pwex 
 |-  ~P U. ran U. E e. _V
28 27 23 xpex 
 |-  ( ~P U. ran U. E X. E ) e. _V
29 simpl 
 |-  ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) -> f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) )
30 fvssunirn 
 |-  ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) C_ U. ran s
31 elssuni 
 |-  ( s e. E -> s C_ U. E )
32 31 adantl 
 |-  ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) -> s C_ U. E )
33 rnss 
 |-  ( s C_ U. E -> ran s C_ ran U. E )
34 uniss 
 |-  ( ran s C_ ran U. E -> U. ran s C_ U. ran U. E )
35 32 33 34 3syl 
 |-  ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) -> U. ran s C_ U. ran U. E )
36 30 35 sstrid 
 |-  ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) -> ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) C_ U. ran U. E )
37 26 elpw2 
 |-  ( ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) e. ~P U. ran U. E <-> ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) C_ U. ran U. E )
38 36 37 sylibr 
 |-  ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) -> ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) e. ~P U. ran U. E )
39 29 38 eqeltrd 
 |-  ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) -> f e. ~P U. ran U. E )
40 simpr 
 |-  ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) -> s e. E )
41 39 40 jca 
 |-  ( ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) -> ( f e. ~P U. ran U. E /\ s e. E ) )
42 41 ssopab2i 
 |-  { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } C_ { <. f , s >. | ( f e. ~P U. ran U. E /\ s e. E ) }
43 df-xp 
 |-  ( ~P U. ran U. E X. E ) = { <. f , s >. | ( f e. ~P U. ran U. E /\ s e. E ) }
44 42 43 sseqtrri 
 |-  { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } C_ ( ~P U. ran U. E X. E )
45 28 44 ssexi 
 |-  { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } e. _V
46 21 22 45 fvmpt 
 |-  ( Q e. { r e. A | -. r .<_ W } -> ( ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) ` Q ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } )
47 15 46 syl 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( q e. { r e. A | -. r .<_ W } |-> { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = q ) ) /\ s e. E ) } ) ` Q ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } )
48 10 47 eqtrd 
 |-  ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } )