Metamath Proof Explorer

Theorem glbconN

Description: De Morgan's law for GLB and LUB. This holds in any complete ortholattice, although we assume HL for convenience. (Contributed by NM, 17-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses glbcon.b 
|- B = ( Base ` K )
glbcon.u 
|- U = ( lub ` K )
glbcon.g 
|- G = ( glb ` K )
glbcon.o 
|- ._|_ = ( oc ` K )
Assertion glbconN 
|- ( ( K e. HL /\ S C_ B ) -> ( G ` S ) = ( ._|_ ` ( U ` { x e. B | ( ._|_ ` x ) e. S } ) ) )

Proof

Step Hyp Ref Expression
1 glbcon.b 
 |-  B = ( Base ` K )
2 glbcon.u 
 |-  U = ( lub ` K )
3 glbcon.g 
 |-  G = ( glb ` K )
4 glbcon.o 
 |-  ._|_ = ( oc ` K )
5 dfin5 
 |-  ( B i^i S ) = { x e. B | x e. S }
6 sseqin2 
 |-  ( S C_ B <-> ( B i^i S ) = S )
7 6 biimpi 
 |-  ( S C_ B -> ( B i^i S ) = S )
8 5 7 syl5reqr 
 |-  ( S C_ B -> S = { x e. B | x e. S } )
9 8 fveq2d 
 |-  ( S C_ B -> ( G ` S ) = ( G ` { x e. B | x e. S } ) )
10 eqid 
 |-  ( le ` K ) = ( le ` K )
11 biid 
 |-  ( ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) <-> ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) )
12 id 
 |-  ( K e. HL -> K e. HL )
13 ssrab2 
 |-  { x e. B | x e. S } C_ B
14 13 a1i 
 |-  ( K e. HL -> { x e. B | x e. S } C_ B )
15 1 10 3 11 12 14 glbval 
 |-  ( K e. HL -> ( G ` { x e. B | x e. S } ) = ( iota_ y e. B ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) ) )
16 hlop 
 |-  ( K e. HL -> K e. OP )
17 hlclat 
 |-  ( K e. HL -> K e. CLat )
18 1 3 clatglbcl 
 |-  ( ( K e. CLat /\ { x e. B | x e. S } C_ B ) -> ( G ` { x e. B | x e. S } ) e. B )
19 17 13 18 sylancl 
 |-  ( K e. HL -> ( G ` { x e. B | x e. S } ) e. B )
20 15 19 eqeltrrd 
 |-  ( K e. HL -> ( iota_ y e. B ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) ) e. B )
21 1 fvexi 
 |-  B e. _V
22 21 riotaclbBAD 
 |-  ( E! y e. B ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) <-> ( iota_ y e. B ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) ) e. B )
23 20 22 sylibr 
 |-  ( K e. HL -> E! y e. B ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) )
24 breq1 
 |-  ( y = ( ._|_ ` v ) -> ( y ( le ` K ) z <-> ( ._|_ ` v ) ( le ` K ) z ) )
25 24 ralbidv 
 |-  ( y = ( ._|_ ` v ) -> ( A. z e. { x e. B | x e. S } y ( le ` K ) z <-> A. z e. { x e. B | x e. S } ( ._|_ ` v ) ( le ` K ) z ) )
26 breq2 
 |-  ( y = ( ._|_ ` v ) -> ( w ( le ` K ) y <-> w ( le ` K ) ( ._|_ ` v ) ) )
27 26 imbi2d 
 |-  ( y = ( ._|_ ` v ) -> ( ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) <-> ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) ) )
28 27 ralbidv 
 |-  ( y = ( ._|_ ` v ) -> ( A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) <-> A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) ) )
29 25 28 anbi12d 
 |-  ( y = ( ._|_ ` v ) -> ( ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) <-> ( A. z e. { x e. B | x e. S } ( ._|_ ` v ) ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) ) ) )
30 1 4 29 riotaocN 
 |-  ( ( K e. OP /\ E! y e. B ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) ) -> ( iota_ y e. B ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) ) = ( ._|_ ` ( iota_ v e. B ( A. z e. { x e. B | x e. S } ( ._|_ ` v ) ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) ) ) ) )
31 16 23 30 syl2anc 
 |-  ( K e. HL -> ( iota_ y e. B ( A. z e. { x e. B | x e. S } y ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) y ) ) ) = ( ._|_ ` ( iota_ v e. B ( A. z e. { x e. B | x e. S } ( ._|_ ` v ) ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) ) ) ) )
32 16 ad2antrr 
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> K e. OP )
33 1 4 opoccl 
 |-  ( ( K e. OP /\ u e. B ) -> ( ._|_ ` u ) e. B )
34 32 33 sylancom 
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> ( ._|_ ` u ) e. B )
35 16 ad2antrr 
 |-  ( ( ( K e. HL /\ v e. B ) /\ z e. B ) -> K e. OP )
36 1 4 opoccl 
 |-  ( ( K e. OP /\ z e. B ) -> ( ._|_ ` z ) e. B )
37 35 36 sylancom 
 |-  ( ( ( K e. HL /\ v e. B ) /\ z e. B ) -> ( ._|_ ` z ) e. B )
38 1 4 opococ 
 |-  ( ( K e. OP /\ z e. B ) -> ( ._|_ ` ( ._|_ ` z ) ) = z )
39 35 38 sylancom 
 |-  ( ( ( K e. HL /\ v e. B ) /\ z e. B ) -> ( ._|_ ` ( ._|_ ` z ) ) = z )
40 39 eqcomd 
 |-  ( ( ( K e. HL /\ v e. B ) /\ z e. B ) -> z = ( ._|_ ` ( ._|_ ` z ) ) )
41 fveq2 
 |-  ( u = ( ._|_ ` z ) -> ( ._|_ ` u ) = ( ._|_ ` ( ._|_ ` z ) ) )
42 41 rspceeqv 
 |-  ( ( ( ._|_ ` z ) e. B /\ z = ( ._|_ ` ( ._|_ ` z ) ) ) -> E. u e. B z = ( ._|_ ` u ) )
43 37 40 42 syl2anc 
 |-  ( ( ( K e. HL /\ v e. B ) /\ z e. B ) -> E. u e. B z = ( ._|_ ` u ) )
44 eleq1 
 |-  ( z = ( ._|_ ` u ) -> ( z e. S <-> ( ._|_ ` u ) e. S ) )
45 breq2 
 |-  ( z = ( ._|_ ` u ) -> ( ( ._|_ ` v ) ( le ` K ) z <-> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) )
46 44 45 imbi12d 
 |-  ( z = ( ._|_ ` u ) -> ( ( z e. S -> ( ._|_ ` v ) ( le ` K ) z ) <-> ( ( ._|_ ` u ) e. S -> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) ) )
47 46 adantl 
 |-  ( ( ( K e. HL /\ v e. B ) /\ z = ( ._|_ ` u ) ) -> ( ( z e. S -> ( ._|_ ` v ) ( le ` K ) z ) <-> ( ( ._|_ ` u ) e. S -> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) ) )
48 34 43 47 ralxfrd 
 |-  ( ( K e. HL /\ v e. B ) -> ( A. z e. B ( z e. S -> ( ._|_ ` v ) ( le ` K ) z ) <-> A. u e. B ( ( ._|_ ` u ) e. S -> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) ) )
49 simpr 
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> u e. B )
50 simplr 
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> v e. B )
51 1 10 4 oplecon3b 
 |-  ( ( K e. OP /\ u e. B /\ v e. B ) -> ( u ( le ` K ) v <-> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) )
52 32 49 50 51 syl3anc 
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> ( u ( le ` K ) v <-> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) )
53 52 imbi2d 
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> ( ( ( ._|_ ` u ) e. S -> u ( le ` K ) v ) <-> ( ( ._|_ ` u ) e. S -> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) ) )
54 53 ralbidva 
 |-  ( ( K e. HL /\ v e. B ) -> ( A. u e. B ( ( ._|_ ` u ) e. S -> u ( le ` K ) v ) <-> A. u e. B ( ( ._|_ ` u ) e. S -> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) ) )
55 48 54 bitr4d 
 |-  ( ( K e. HL /\ v e. B ) -> ( A. z e. B ( z e. S -> ( ._|_ ` v ) ( le ` K ) z ) <-> A. u e. B ( ( ._|_ ` u ) e. S -> u ( le ` K ) v ) ) )
56 eleq1 
 |-  ( x = z -> ( x e. S <-> z e. S ) )
57 56 ralrab 
 |-  ( A. z e. { x e. B | x e. S } ( ._|_ ` v ) ( le ` K ) z <-> A. z e. B ( z e. S -> ( ._|_ ` v ) ( le ` K ) z ) )
58 fveq2 
 |-  ( x = u -> ( ._|_ ` x ) = ( ._|_ ` u ) )
59 58 eleq1d 
 |-  ( x = u -> ( ( ._|_ ` x ) e. S <-> ( ._|_ ` u ) e. S ) )
60 59 ralrab 
 |-  ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) v <-> A. u e. B ( ( ._|_ ` u ) e. S -> u ( le ` K ) v ) )
61 55 57 60 3bitr4g 
 |-  ( ( K e. HL /\ v e. B ) -> ( A. z e. { x e. B | x e. S } ( ._|_ ` v ) ( le ` K ) z <-> A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) v ) )
62 16 ad2antrr 
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> K e. OP )
63 1 4 opoccl 
 |-  ( ( K e. OP /\ t e. B ) -> ( ._|_ ` t ) e. B )
64 62 63 sylancom 
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> ( ._|_ ` t ) e. B )
65 16 ad2antrr 
 |-  ( ( ( K e. HL /\ v e. B ) /\ w e. B ) -> K e. OP )
66 1 4 opoccl 
 |-  ( ( K e. OP /\ w e. B ) -> ( ._|_ ` w ) e. B )
67 65 66 sylancom 
 |-  ( ( ( K e. HL /\ v e. B ) /\ w e. B ) -> ( ._|_ ` w ) e. B )
68 1 4 opococ 
 |-  ( ( K e. OP /\ w e. B ) -> ( ._|_ ` ( ._|_ ` w ) ) = w )
69 65 68 sylancom 
 |-  ( ( ( K e. HL /\ v e. B ) /\ w e. B ) -> ( ._|_ ` ( ._|_ ` w ) ) = w )
70 69 eqcomd 
 |-  ( ( ( K e. HL /\ v e. B ) /\ w e. B ) -> w = ( ._|_ ` ( ._|_ ` w ) ) )
71 fveq2 
 |-  ( t = ( ._|_ ` w ) -> ( ._|_ ` t ) = ( ._|_ ` ( ._|_ ` w ) ) )
72 71 rspceeqv 
 |-  ( ( ( ._|_ ` w ) e. B /\ w = ( ._|_ ` ( ._|_ ` w ) ) ) -> E. t e. B w = ( ._|_ ` t ) )
73 67 70 72 syl2anc 
 |-  ( ( ( K e. HL /\ v e. B ) /\ w e. B ) -> E. t e. B w = ( ._|_ ` t ) )
74 breq1 
 |-  ( w = ( ._|_ ` t ) -> ( w ( le ` K ) z <-> ( ._|_ ` t ) ( le ` K ) z ) )
75 74 ralbidv 
 |-  ( w = ( ._|_ ` t ) -> ( A. z e. { x e. B | x e. S } w ( le ` K ) z <-> A. z e. { x e. B | x e. S } ( ._|_ ` t ) ( le ` K ) z ) )
76 breq1 
 |-  ( w = ( ._|_ ` t ) -> ( w ( le ` K ) ( ._|_ ` v ) <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) )
77 75 76 imbi12d 
 |-  ( w = ( ._|_ ` t ) -> ( ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) <-> ( A. z e. { x e. B | x e. S } ( ._|_ ` t ) ( le ` K ) z -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) ) )
78 77 adantl 
 |-  ( ( ( K e. HL /\ v e. B ) /\ w = ( ._|_ ` t ) ) -> ( ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) <-> ( A. z e. { x e. B | x e. S } ( ._|_ ` t ) ( le ` K ) z -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) ) )
79 64 73 78 ralxfrd 
 |-  ( ( K e. HL /\ v e. B ) -> ( A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) <-> A. t e. B ( A. z e. { x e. B | x e. S } ( ._|_ ` t ) ( le ` K ) z -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) ) )
80 16 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> K e. OP )
81 simpr 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> u e. B )
82 simplr 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> t e. B )
83 1 10 4 oplecon3b 
 |-  ( ( K e. OP /\ u e. B /\ t e. B ) -> ( u ( le ` K ) t <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) )
84 80 81 82 83 syl3anc 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> ( u ( le ` K ) t <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) )
85 84 imbi2d 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> ( ( ( ._|_ ` u ) e. S -> u ( le ` K ) t ) <-> ( ( ._|_ ` u ) e. S -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) ) )
86 85 ralbidva 
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> ( A. u e. B ( ( ._|_ ` u ) e. S -> u ( le ` K ) t ) <-> A. u e. B ( ( ._|_ ` u ) e. S -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) ) )
87 80 33 sylancom 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> ( ._|_ ` u ) e. B )
88 16 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z e. B ) -> K e. OP )
89 88 36 sylancom 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z e. B ) -> ( ._|_ ` z ) e. B )
90 88 38 sylancom 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z e. B ) -> ( ._|_ ` ( ._|_ ` z ) ) = z )
91 90 eqcomd 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z e. B ) -> z = ( ._|_ ` ( ._|_ ` z ) ) )
92 89 91 42 syl2anc 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z e. B ) -> E. u e. B z = ( ._|_ ` u ) )
93 breq2 
 |-  ( z = ( ._|_ ` u ) -> ( ( ._|_ ` t ) ( le ` K ) z <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) )
94 44 93 imbi12d 
 |-  ( z = ( ._|_ ` u ) -> ( ( z e. S -> ( ._|_ ` t ) ( le ` K ) z ) <-> ( ( ._|_ ` u ) e. S -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) ) )
95 94 adantl 
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z = ( ._|_ ` u ) ) -> ( ( z e. S -> ( ._|_ ` t ) ( le ` K ) z ) <-> ( ( ._|_ ` u ) e. S -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) ) )
96 87 92 95 ralxfrd 
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> ( A. z e. B ( z e. S -> ( ._|_ ` t ) ( le ` K ) z ) <-> A. u e. B ( ( ._|_ ` u ) e. S -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) ) )
97 86 96 bitr4d 
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> ( A. u e. B ( ( ._|_ ` u ) e. S -> u ( le ` K ) t ) <-> A. z e. B ( z e. S -> ( ._|_ ` t ) ( le ` K ) z ) ) )
98 59 ralrab 
 |-  ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t <-> A. u e. B ( ( ._|_ ` u ) e. S -> u ( le ` K ) t ) )
99 56 ralrab 
 |-  ( A. z e. { x e. B | x e. S } ( ._|_ ` t ) ( le ` K ) z <-> A. z e. B ( z e. S -> ( ._|_ ` t ) ( le ` K ) z ) )
100 97 98 99 3bitr4g 
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t <-> A. z e. { x e. B | x e. S } ( ._|_ ` t ) ( le ` K ) z ) )
101 simplr 
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> v e. B )
102 simpr 
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> t e. B )
103 1 10 4 oplecon3b 
 |-  ( ( K e. OP /\ v e. B /\ t e. B ) -> ( v ( le ` K ) t <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) )
104 62 101 102 103 syl3anc 
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> ( v ( le ` K ) t <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) )
105 100 104 imbi12d 
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> ( ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t -> v ( le ` K ) t ) <-> ( A. z e. { x e. B | x e. S } ( ._|_ ` t ) ( le ` K ) z -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) ) )
106 105 ralbidva 
 |-  ( ( K e. HL /\ v e. B ) -> ( A. t e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t -> v ( le ` K ) t ) <-> A. t e. B ( A. z e. { x e. B | x e. S } ( ._|_ ` t ) ( le ` K ) z -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) ) )
107 79 106 bitr4d 
 |-  ( ( K e. HL /\ v e. B ) -> ( A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) <-> A. t e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t -> v ( le ` K ) t ) ) )
108 61 107 anbi12d 
 |-  ( ( K e. HL /\ v e. B ) -> ( ( A. z e. { x e. B | x e. S } ( ._|_ ` v ) ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) ) <-> ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) v /\ A. t e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t -> v ( le ` K ) t ) ) ) )
109 108 riotabidva 
 |-  ( K e. HL -> ( iota_ v e. B ( A. z e. { x e. B | x e. S } ( ._|_ ` v ) ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) ) ) = ( iota_ v e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) v /\ A. t e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t -> v ( le ` K ) t ) ) ) )
110 ssrab2 
 |-  { x e. B | ( ._|_ ` x ) e. S } C_ B
111 biid 
 |-  ( ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) v /\ A. t e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t -> v ( le ` K ) t ) ) <-> ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) v /\ A. t e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t -> v ( le ` K ) t ) ) )
112 simpl 
 |-  ( ( K e. HL /\ { x e. B | ( ._|_ ` x ) e. S } C_ B ) -> K e. HL )
113 simpr 
 |-  ( ( K e. HL /\ { x e. B | ( ._|_ ` x ) e. S } C_ B ) -> { x e. B | ( ._|_ ` x ) e. S } C_ B )
114 1 10 2 111 112 113 lubval 
 |-  ( ( K e. HL /\ { x e. B | ( ._|_ ` x ) e. S } C_ B ) -> ( U ` { x e. B | ( ._|_ ` x ) e. S } ) = ( iota_ v e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) v /\ A. t e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t -> v ( le ` K ) t ) ) ) )
115 110 114 mpan2 
 |-  ( K e. HL -> ( U ` { x e. B | ( ._|_ ` x ) e. S } ) = ( iota_ v e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) v /\ A. t e. B ( A. u e. { x e. B | ( ._|_ ` x ) e. S } u ( le ` K ) t -> v ( le ` K ) t ) ) ) )
116 109 115 eqtr4d 
 |-  ( K e. HL -> ( iota_ v e. B ( A. z e. { x e. B | x e. S } ( ._|_ ` v ) ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) ) ) = ( U ` { x e. B | ( ._|_ ` x ) e. S } ) )
117 116 fveq2d 
 |-  ( K e. HL -> ( ._|_ ` ( iota_ v e. B ( A. z e. { x e. B | x e. S } ( ._|_ ` v ) ( le ` K ) z /\ A. w e. B ( A. z e. { x e. B | x e. S } w ( le ` K ) z -> w ( le ` K ) ( ._|_ ` v ) ) ) ) ) = ( ._|_ ` ( U ` { x e. B | ( ._|_ ` x ) e. S } ) ) )
118 15 31 117 3eqtrd 
 |-  ( K e. HL -> ( G ` { x e. B | x e. S } ) = ( ._|_ ` ( U ` { x e. B | ( ._|_ ` x ) e. S } ) ) )
119 9 118 sylan9eqr 
 |-  ( ( K e. HL /\ S C_ B ) -> ( G ` S ) = ( ._|_ ` ( U ` { x e. B | ( ._|_ ` x ) e. S } ) ) )