This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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