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 df-riota . (Revised by SN, 3-Jan-2025) (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 sseqin2
 |-  ( S C_ B <-> ( B i^i S ) = S )
6 5 biimpi
 |-  ( S C_ B -> ( B i^i S ) = S )
7 dfin5
 |-  ( B i^i S ) = { x e. B | x e. S }
8 6 7 eqtr3di
 |-  ( 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 clatglbcl2
 |-  ( ( K e. CLat /\ { x e. B | x e. S } C_ B ) -> { x e. B | x e. S } e. dom G )
19 17 14 18 syl2anc
 |-  ( K e. HL -> { x e. B | x e. S } e. dom G )
20 1 10 3 11 12 19 glbeu
 |-  ( 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 ) ) )
21 breq1
 |-  ( y = ( ._|_ ` v ) -> ( y ( le ` K ) z <-> ( ._|_ ` v ) ( le ` K ) z ) )
22 21 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 ) )
23 breq2
 |-  ( y = ( ._|_ ` v ) -> ( w ( le ` K ) y <-> w ( le ` K ) ( ._|_ ` v ) ) )
24 23 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 ) ) ) )
25 24 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 ) ) ) )
26 22 25 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 ) ) ) ) )
27 1 4 26 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 ) ) ) ) ) )
28 16 20 27 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 ) ) ) ) ) )
29 16 ad2antrr
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> K e. OP )
30 1 4 opoccl
 |-  ( ( K e. OP /\ u e. B ) -> ( ._|_ ` u ) e. B )
31 29 30 sylancom
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> ( ._|_ ` u ) e. B )
32 16 ad2antrr
 |-  ( ( ( K e. HL /\ v e. B ) /\ z e. B ) -> K e. OP )
33 1 4 opoccl
 |-  ( ( K e. OP /\ z e. B ) -> ( ._|_ ` z ) e. B )
34 32 33 sylancom
 |-  ( ( ( K e. HL /\ v e. B ) /\ z e. B ) -> ( ._|_ ` z ) e. B )
35 1 4 opococ
 |-  ( ( K e. OP /\ z e. B ) -> ( ._|_ ` ( ._|_ ` z ) ) = z )
36 32 35 sylancom
 |-  ( ( ( K e. HL /\ v e. B ) /\ z e. B ) -> ( ._|_ ` ( ._|_ ` z ) ) = z )
37 36 eqcomd
 |-  ( ( ( K e. HL /\ v e. B ) /\ z e. B ) -> z = ( ._|_ ` ( ._|_ ` z ) ) )
38 fveq2
 |-  ( u = ( ._|_ ` z ) -> ( ._|_ ` u ) = ( ._|_ ` ( ._|_ ` z ) ) )
39 38 rspceeqv
 |-  ( ( ( ._|_ ` z ) e. B /\ z = ( ._|_ ` ( ._|_ ` z ) ) ) -> E. u e. B z = ( ._|_ ` u ) )
40 34 37 39 syl2anc
 |-  ( ( ( K e. HL /\ v e. B ) /\ z e. B ) -> E. u e. B z = ( ._|_ ` u ) )
41 eleq1
 |-  ( z = ( ._|_ ` u ) -> ( z e. S <-> ( ._|_ ` u ) e. S ) )
42 breq2
 |-  ( z = ( ._|_ ` u ) -> ( ( ._|_ ` v ) ( le ` K ) z <-> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) )
43 41 42 imbi12d
 |-  ( z = ( ._|_ ` u ) -> ( ( z e. S -> ( ._|_ ` v ) ( le ` K ) z ) <-> ( ( ._|_ ` u ) e. S -> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) ) )
44 43 adantl
 |-  ( ( ( K e. HL /\ v e. B ) /\ z = ( ._|_ ` u ) ) -> ( ( z e. S -> ( ._|_ ` v ) ( le ` K ) z ) <-> ( ( ._|_ ` u ) e. S -> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) ) )
45 31 40 44 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 ) ) ) )
46 simpr
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> u e. B )
47 simplr
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> v e. B )
48 1 10 4 oplecon3b
 |-  ( ( K e. OP /\ u e. B /\ v e. B ) -> ( u ( le ` K ) v <-> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) )
49 29 46 47 48 syl3anc
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> ( u ( le ` K ) v <-> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) )
50 49 imbi2d
 |-  ( ( ( K e. HL /\ v e. B ) /\ u e. B ) -> ( ( ( ._|_ ` u ) e. S -> u ( le ` K ) v ) <-> ( ( ._|_ ` u ) e. S -> ( ._|_ ` v ) ( le ` K ) ( ._|_ ` u ) ) ) )
51 50 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 ) ) ) )
52 45 51 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 ) ) )
53 eleq1
 |-  ( x = z -> ( x e. S <-> z e. S ) )
54 53 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 ) )
55 fveq2
 |-  ( x = u -> ( ._|_ ` x ) = ( ._|_ ` u ) )
56 55 eleq1d
 |-  ( x = u -> ( ( ._|_ ` x ) e. S <-> ( ._|_ ` u ) e. S ) )
57 56 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 ) )
58 52 54 57 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 ) )
59 16 ad2antrr
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> K e. OP )
60 1 4 opoccl
 |-  ( ( K e. OP /\ t e. B ) -> ( ._|_ ` t ) e. B )
61 59 60 sylancom
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> ( ._|_ ` t ) e. B )
62 16 ad2antrr
 |-  ( ( ( K e. HL /\ v e. B ) /\ w e. B ) -> K e. OP )
63 1 4 opoccl
 |-  ( ( K e. OP /\ w e. B ) -> ( ._|_ ` w ) e. B )
64 62 63 sylancom
 |-  ( ( ( K e. HL /\ v e. B ) /\ w e. B ) -> ( ._|_ ` w ) e. B )
65 1 4 opococ
 |-  ( ( K e. OP /\ w e. B ) -> ( ._|_ ` ( ._|_ ` w ) ) = w )
66 62 65 sylancom
 |-  ( ( ( K e. HL /\ v e. B ) /\ w e. B ) -> ( ._|_ ` ( ._|_ ` w ) ) = w )
67 66 eqcomd
 |-  ( ( ( K e. HL /\ v e. B ) /\ w e. B ) -> w = ( ._|_ ` ( ._|_ ` w ) ) )
68 fveq2
 |-  ( t = ( ._|_ ` w ) -> ( ._|_ ` t ) = ( ._|_ ` ( ._|_ ` w ) ) )
69 68 rspceeqv
 |-  ( ( ( ._|_ ` w ) e. B /\ w = ( ._|_ ` ( ._|_ ` w ) ) ) -> E. t e. B w = ( ._|_ ` t ) )
70 64 67 69 syl2anc
 |-  ( ( ( K e. HL /\ v e. B ) /\ w e. B ) -> E. t e. B w = ( ._|_ ` t ) )
71 breq1
 |-  ( w = ( ._|_ ` t ) -> ( w ( le ` K ) z <-> ( ._|_ ` t ) ( le ` K ) z ) )
72 71 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 ) )
73 breq1
 |-  ( w = ( ._|_ ` t ) -> ( w ( le ` K ) ( ._|_ ` v ) <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) )
74 72 73 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 ) ) ) )
75 74 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 ) ) ) )
76 61 70 75 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 ) ) ) )
77 16 ad3antrrr
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> K e. OP )
78 simpr
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> u e. B )
79 simplr
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> t e. B )
80 1 10 4 oplecon3b
 |-  ( ( K e. OP /\ u e. B /\ t e. B ) -> ( u ( le ` K ) t <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) )
81 77 78 79 80 syl3anc
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> ( u ( le ` K ) t <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) )
82 81 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 ) ) ) )
83 82 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 ) ) ) )
84 77 30 sylancom
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ u e. B ) -> ( ._|_ ` u ) e. B )
85 16 ad3antrrr
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z e. B ) -> K e. OP )
86 85 33 sylancom
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z e. B ) -> ( ._|_ ` z ) e. B )
87 85 35 sylancom
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z e. B ) -> ( ._|_ ` ( ._|_ ` z ) ) = z )
88 87 eqcomd
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z e. B ) -> z = ( ._|_ ` ( ._|_ ` z ) ) )
89 86 88 39 syl2anc
 |-  ( ( ( ( K e. HL /\ v e. B ) /\ t e. B ) /\ z e. B ) -> E. u e. B z = ( ._|_ ` u ) )
90 breq2
 |-  ( z = ( ._|_ ` u ) -> ( ( ._|_ ` t ) ( le ` K ) z <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) )
91 41 90 imbi12d
 |-  ( z = ( ._|_ ` u ) -> ( ( z e. S -> ( ._|_ ` t ) ( le ` K ) z ) <-> ( ( ._|_ ` u ) e. S -> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` u ) ) ) )
92 91 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 ) ) ) )
93 84 89 92 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 ) ) ) )
94 83 93 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 ) ) )
95 56 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 ) )
96 53 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 ) )
97 94 95 96 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 ) )
98 simplr
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> v e. B )
99 simpr
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> t e. B )
100 1 10 4 oplecon3b
 |-  ( ( K e. OP /\ v e. B /\ t e. B ) -> ( v ( le ` K ) t <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) )
101 59 98 99 100 syl3anc
 |-  ( ( ( K e. HL /\ v e. B ) /\ t e. B ) -> ( v ( le ` K ) t <-> ( ._|_ ` t ) ( le ` K ) ( ._|_ ` v ) ) )
102 97 101 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 ) ) ) )
103 102 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 ) ) ) )
104 76 103 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 ) ) )
105 58 104 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 ) ) ) )
106 105 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 ) ) ) )
107 ssrab2
 |-  { x e. B | ( ._|_ ` x ) e. S } C_ B
108 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 ) ) )
109 simpl
 |-  ( ( K e. HL /\ { x e. B | ( ._|_ ` x ) e. S } C_ B ) -> K e. HL )
110 simpr
 |-  ( ( K e. HL /\ { x e. B | ( ._|_ ` x ) e. S } C_ B ) -> { x e. B | ( ._|_ ` x ) e. S } C_ B )
111 1 10 2 108 109 110 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 ) ) ) )
112 107 111 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 ) ) ) )
113 106 112 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 } ) )
114 113 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 } ) ) )
115 15 28 114 3eqtrd
 |-  ( K e. HL -> ( G ` { x e. B | x e. S } ) = ( ._|_ ` ( U ` { x e. B | ( ._|_ ` x ) e. S } ) ) )
116 9 115 sylan9eqr
 |-  ( ( K e. HL /\ S C_ B ) -> ( G ` S ) = ( ._|_ ` ( U ` { x e. B | ( ._|_ ` x ) e. S } ) ) )