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