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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
glbcon.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
glbcon.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
glbcon.o ⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion glbconN ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) ) )

Proof

Step Hyp Ref Expression
1 glbcon.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 glbcon.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
3 glbcon.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
4 glbcon.o ⊢ ⊥ = ( oc ‘ 𝐾 )
5 sseqin2 ⊢ ( 𝑆 ⊆ 𝐵 ↔ ( 𝐵 ∩ 𝑆 ) = 𝑆 )
6 5 biimpi ⊢ ( 𝑆 ⊆ 𝐵 → ( 𝐵 ∩ 𝑆 ) = 𝑆 )
7 dfin5 ⊢ ( 𝐵 ∩ 𝑆 ) = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 }
8 6 7 eqtr3di ⊢ ( 𝑆 ⊆ 𝐵 → 𝑆 = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } )
9 8 fveq2d ⊢ ( 𝑆 ⊆ 𝐵 → ( 𝐺 ‘ 𝑆 ) = ( 𝐺 ‘ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ) )
10 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
11 biid ⊢ ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) )
12 id ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ HL )
13 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ⊆ 𝐵
14 13 a1i ⊢ ( 𝐾 ∈ HL → { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ⊆ 𝐵 )
15 1 10 3 11 12 14 glbval ⊢ ( 𝐾 ∈ HL → ( 𝐺 ‘ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ) = ( ℩ 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ) )
16 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
17 hlclat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CLat )
18 1 3 clatglbcl2 ⊢ ( ( 𝐾 ∈ CLat ∧ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ⊆ 𝐵 ) → { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ∈ dom 𝐺 )
19 17 14 18 syl2anc ⊢ ( 𝐾 ∈ HL → { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ∈ dom 𝐺 )
20 1 10 3 11 12 19 glbeu ⊢ ( 𝐾 ∈ HL → ∃! 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) )
21 breq1 ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( 𝑦 ( le ‘ 𝐾 ) 𝑧 ↔ ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) )
22 21 ralbidv ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) )
23 breq2 ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( 𝑤 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) )
24 23 imbi2d ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
25 24 ralbidv ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ↔ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
26 22 25 anbi12d ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) )
27 1 4 26 riotaocN ⊢ ( ( 𝐾 ∈ OP ∧ ∃! 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ) → ( ℩ 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ) = ( ⊥ ‘ ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) ) )
28 16 20 27 syl2anc ⊢ ( 𝐾 ∈ HL → ( ℩ 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ) = ( ⊥ ‘ ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) ) )
29 16 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝐾 ∈ OP )
30 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵 ) → ( ⊥ ‘ 𝑢 ) ∈ 𝐵 )
31 29 30 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ⊥ ‘ 𝑢 ) ∈ 𝐵 )
32 16 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ OP )
33 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ 𝑧 ) ∈ 𝐵 )
34 32 33 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ 𝑧 ) ∈ 𝐵 )
35 1 4 opococ ⊢ ( ( 𝐾 ∈ OP ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) = 𝑧 )
36 32 35 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) = 𝑧 )
37 36 eqcomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 = ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) )
38 fveq2 ⊢ ( 𝑢 = ( ⊥ ‘ 𝑧 ) → ( ⊥ ‘ 𝑢 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) )
39 38 rspceeqv ⊢ ( ( ( ⊥ ‘ 𝑧 ) ∈ 𝐵 ∧ 𝑧 = ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) ) → ∃ 𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘ 𝑢 ) )
40 34 37 39 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘ 𝑢 ) )
41 eleq1 ⊢ ( 𝑧 = ( ⊥ ‘ 𝑢 ) → ( 𝑧 ∈ 𝑆 ↔ ( ⊥ ‘ 𝑢 ) ∈ 𝑆 ) )
42 breq2 ⊢ ( 𝑧 = ( ⊥ ‘ 𝑢 ) → ( ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ↔ ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
43 41 42 imbi12d ⊢ ( 𝑧 = ( ⊥ ‘ 𝑢 ) → ( ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
44 43 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 = ( ⊥ ‘ 𝑢 ) ) → ( ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
45 31 40 44 ralxfrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
46 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
47 simplr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑣 ∈ 𝐵 )
48 1 10 4 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ( le ‘ 𝐾 ) 𝑣 ↔ ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
49 29 46 47 48 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑢 ( le ‘ 𝐾 ) 𝑣 ↔ ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
50 49 imbi2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑣 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
51 50 ralbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑣 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
52 45 51 bitr4d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑣 ) ) )
53 eleq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑆 ↔ 𝑧 ∈ 𝑆 ) )
54 53 ralrab ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) )
55 fveq2 ⊢ ( 𝑥 = 𝑢 → ( ⊥ ‘ 𝑥 ) = ( ⊥ ‘ 𝑢 ) )
56 55 eleq1d ⊢ ( 𝑥 = 𝑢 → ( ( ⊥ ‘ 𝑥 ) ∈ 𝑆 ↔ ( ⊥ ‘ 𝑢 ) ∈ 𝑆 ) )
57 56 ralrab ⊢ ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑣 ) )
58 52 54 57 3bitr4g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ) )
59 16 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → 𝐾 ∈ OP )
60 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑡 ∈ 𝐵 ) → ( ⊥ ‘ 𝑡 ) ∈ 𝐵 )
61 59 60 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ⊥ ‘ 𝑡 ) ∈ 𝐵 )
62 16 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) → 𝐾 ∈ OP )
63 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑤 ∈ 𝐵 ) → ( ⊥ ‘ 𝑤 ) ∈ 𝐵 )
64 62 63 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) → ( ⊥ ‘ 𝑤 ) ∈ 𝐵 )
65 1 4 opococ ⊢ ( ( 𝐾 ∈ OP ∧ 𝑤 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑤 ) ) = 𝑤 )
66 62 65 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑤 ) ) = 𝑤 )
67 66 eqcomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) → 𝑤 = ( ⊥ ‘ ( ⊥ ‘ 𝑤 ) ) )
68 fveq2 ⊢ ( 𝑡 = ( ⊥ ‘ 𝑤 ) → ( ⊥ ‘ 𝑡 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑤 ) ) )
69 68 rspceeqv ⊢ ( ( ( ⊥ ‘ 𝑤 ) ∈ 𝐵 ∧ 𝑤 = ( ⊥ ‘ ( ⊥ ‘ 𝑤 ) ) ) → ∃ 𝑡 ∈ 𝐵 𝑤 = ( ⊥ ‘ 𝑡 ) )
70 64 67 69 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑡 ∈ 𝐵 𝑤 = ( ⊥ ‘ 𝑡 ) )
71 breq1 ⊢ ( 𝑤 = ( ⊥ ‘ 𝑡 ) → ( 𝑤 ( le ‘ 𝐾 ) 𝑧 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) )
72 71 ralbidv ⊢ ( 𝑤 = ( ⊥ ‘ 𝑡 ) → ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) )
73 breq1 ⊢ ( 𝑤 = ( ⊥ ‘ 𝑡 ) → ( 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) )
74 72 73 imbi12d ⊢ ( 𝑤 = ( ⊥ ‘ 𝑡 ) → ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
75 74 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 = ( ⊥ ‘ 𝑡 ) ) → ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
76 61 70 75 ralxfrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ↔ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
77 16 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝐾 ∈ OP )
78 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
79 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑡 ∈ 𝐵 )
80 1 10 4 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) → ( 𝑢 ( le ‘ 𝐾 ) 𝑡 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
81 77 78 79 80 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑢 ( le ‘ 𝐾 ) 𝑡 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
82 81 imbi2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑡 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
83 82 ralbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑡 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
84 77 30 sylancom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ⊥ ‘ 𝑢 ) ∈ 𝐵 )
85 16 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ OP )
86 85 33 sylancom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ 𝑧 ) ∈ 𝐵 )
87 85 35 sylancom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) = 𝑧 )
88 87 eqcomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 = ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) )
89 86 88 39 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘ 𝑢 ) )
90 breq2 ⊢ ( 𝑧 = ( ⊥ ‘ 𝑢 ) → ( ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
91 41 90 imbi12d ⊢ ( 𝑧 = ( ⊥ ‘ 𝑢 ) → ( ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
92 91 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 = ( ⊥ ‘ 𝑢 ) ) → ( ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
93 84 89 92 ralxfrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
94 83 93 bitr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑡 ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) ) )
95 56 ralrab ⊢ ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑡 ) )
96 53 ralrab ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) )
97 94 95 96 3bitr4g ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) )
98 simplr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → 𝑣 ∈ 𝐵 )
99 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → 𝑡 ∈ 𝐵 )
100 1 10 4 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑣 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) → ( 𝑣 ( le ‘ 𝐾 ) 𝑡 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) )
101 59 98 99 100 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( 𝑣 ( le ‘ 𝐾 ) 𝑡 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) )
102 97 101 imbi12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
103 102 ralbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ↔ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
104 76 103 bitr4d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ↔ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) )
105 58 104 anbi12d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ↔ ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) ) )
106 105 riotabidva ⊢ ( 𝐾 ∈ HL → ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) = ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) ) )
107 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ⊆ 𝐵
108 biid ⊢ ( ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) ↔ ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) )
109 simpl ⊢ ( ( 𝐾 ∈ HL ∧ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ⊆ 𝐵 ) → 𝐾 ∈ HL )
110 simpr ⊢ ( ( 𝐾 ∈ HL ∧ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ⊆ 𝐵 ) → { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ⊆ 𝐵 )
111 1 10 2 108 109 110 lubval ⊢ ( ( 𝐾 ∈ HL ∧ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ⊆ 𝐵 ) → ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) = ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) ) )
112 107 111 mpan2 ⊢ ( 𝐾 ∈ HL → ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) = ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) ) )
113 106 112 eqtr4d ⊢ ( 𝐾 ∈ HL → ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) = ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) )
114 113 fveq2d ⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) ) )
115 15 28 114 3eqtrd ⊢ ( 𝐾 ∈ HL → ( 𝐺 ‘ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) ) )
116 9 115 sylan9eqr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) ) )