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 ⊢ 𝐵 = ( 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 clatglbcl ⊢ ( ( 𝐾 ∈ CLat ∧ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ⊆ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ) ∈ 𝐵 )
19 17 13 18 sylancl ⊢ ( 𝐾 ∈ HL → ( 𝐺 ‘ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ) ∈ 𝐵 )
20 15 19 eqeltrrd ⊢ ( 𝐾 ∈ HL → ( ℩ 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ) ∈ 𝐵 )
21 1 fvexi ⊢ 𝐵 ∈ V
22 21 riotaclbBAD ⊢ ( ∃! 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ↔ ( ℩ 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ) ∈ 𝐵 )
23 20 22 sylibr ⊢ ( 𝐾 ∈ HL → ∃! 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) )
24 breq1 ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( 𝑦 ( le ‘ 𝐾 ) 𝑧 ↔ ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) )
25 24 ralbidv ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) )
26 breq2 ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( 𝑤 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) )
27 26 imbi2d ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
28 27 ralbidv ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ↔ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
29 25 28 anbi12d ⊢ ( 𝑦 = ( ⊥ ‘ 𝑣 ) → ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) )
30 1 4 29 riotaocN ⊢ ( ( 𝐾 ∈ OP ∧ ∃! 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ) → ( ℩ 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ) = ( ⊥ ‘ ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) ) )
31 16 23 30 syl2anc ⊢ ( 𝐾 ∈ HL → ( ℩ 𝑦 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑦 ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) 𝑦 ) ) ) = ( ⊥ ‘ ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) ) )
32 16 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝐾 ∈ OP )
33 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵 ) → ( ⊥ ‘ 𝑢 ) ∈ 𝐵 )
34 32 33 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ⊥ ‘ 𝑢 ) ∈ 𝐵 )
35 16 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ OP )
36 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ 𝑧 ) ∈ 𝐵 )
37 35 36 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ 𝑧 ) ∈ 𝐵 )
38 1 4 opococ ⊢ ( ( 𝐾 ∈ OP ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) = 𝑧 )
39 35 38 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) = 𝑧 )
40 39 eqcomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 = ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) )
41 fveq2 ⊢ ( 𝑢 = ( ⊥ ‘ 𝑧 ) → ( ⊥ ‘ 𝑢 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) )
42 41 rspceeqv ⊢ ( ( ( ⊥ ‘ 𝑧 ) ∈ 𝐵 ∧ 𝑧 = ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) ) → ∃ 𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘ 𝑢 ) )
43 37 40 42 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘ 𝑢 ) )
44 eleq1 ⊢ ( 𝑧 = ( ⊥ ‘ 𝑢 ) → ( 𝑧 ∈ 𝑆 ↔ ( ⊥ ‘ 𝑢 ) ∈ 𝑆 ) )
45 breq2 ⊢ ( 𝑧 = ( ⊥ ‘ 𝑢 ) → ( ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ↔ ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
46 44 45 imbi12d ⊢ ( 𝑧 = ( ⊥ ‘ 𝑢 ) → ( ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
47 46 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑧 = ( ⊥ ‘ 𝑢 ) ) → ( ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
48 34 43 47 ralxfrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
49 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
50 simplr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑣 ∈ 𝐵 )
51 1 10 4 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) → ( 𝑢 ( le ‘ 𝐾 ) 𝑣 ↔ ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
52 32 49 50 51 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑢 ( le ‘ 𝐾 ) 𝑣 ↔ ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
53 52 imbi2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑣 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
54 53 ralbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑣 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
55 48 54 bitr4d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑣 ) ) )
56 eleq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑆 ↔ 𝑧 ∈ 𝑆 ) )
57 56 ralrab ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ) )
58 fveq2 ⊢ ( 𝑥 = 𝑢 → ( ⊥ ‘ 𝑥 ) = ( ⊥ ‘ 𝑢 ) )
59 58 eleq1d ⊢ ( 𝑥 = 𝑢 → ( ( ⊥ ‘ 𝑥 ) ∈ 𝑆 ↔ ( ⊥ ‘ 𝑢 ) ∈ 𝑆 ) )
60 59 ralrab ⊢ ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑣 ) )
61 55 57 60 3bitr4g ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ) )
62 16 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → 𝐾 ∈ OP )
63 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑡 ∈ 𝐵 ) → ( ⊥ ‘ 𝑡 ) ∈ 𝐵 )
64 62 63 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ⊥ ‘ 𝑡 ) ∈ 𝐵 )
65 16 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) → 𝐾 ∈ OP )
66 1 4 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑤 ∈ 𝐵 ) → ( ⊥ ‘ 𝑤 ) ∈ 𝐵 )
67 65 66 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) → ( ⊥ ‘ 𝑤 ) ∈ 𝐵 )
68 1 4 opococ ⊢ ( ( 𝐾 ∈ OP ∧ 𝑤 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑤 ) ) = 𝑤 )
69 65 68 sylancom ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑤 ) ) = 𝑤 )
70 69 eqcomd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) → 𝑤 = ( ⊥ ‘ ( ⊥ ‘ 𝑤 ) ) )
71 fveq2 ⊢ ( 𝑡 = ( ⊥ ‘ 𝑤 ) → ( ⊥ ‘ 𝑡 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑤 ) ) )
72 71 rspceeqv ⊢ ( ( ( ⊥ ‘ 𝑤 ) ∈ 𝐵 ∧ 𝑤 = ( ⊥ ‘ ( ⊥ ‘ 𝑤 ) ) ) → ∃ 𝑡 ∈ 𝐵 𝑤 = ( ⊥ ‘ 𝑡 ) )
73 67 70 72 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑡 ∈ 𝐵 𝑤 = ( ⊥ ‘ 𝑡 ) )
74 breq1 ⊢ ( 𝑤 = ( ⊥ ‘ 𝑡 ) → ( 𝑤 ( le ‘ 𝐾 ) 𝑧 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) )
75 74 ralbidv ⊢ ( 𝑤 = ( ⊥ ‘ 𝑡 ) → ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) )
76 breq1 ⊢ ( 𝑤 = ( ⊥ ‘ 𝑡 ) → ( 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) )
77 75 76 imbi12d ⊢ ( 𝑤 = ( ⊥ ‘ 𝑡 ) → ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
78 77 adantl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑤 = ( ⊥ ‘ 𝑡 ) ) → ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
79 64 73 78 ralxfrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ↔ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
80 16 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝐾 ∈ OP )
81 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
82 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → 𝑡 ∈ 𝐵 )
83 1 10 4 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) → ( 𝑢 ( le ‘ 𝐾 ) 𝑡 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
84 80 81 82 83 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( 𝑢 ( le ‘ 𝐾 ) 𝑡 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
85 84 imbi2d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑡 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
86 85 ralbidva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑡 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
87 80 33 sylancom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑢 ∈ 𝐵 ) → ( ⊥ ‘ 𝑢 ) ∈ 𝐵 )
88 16 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐾 ∈ OP )
89 88 36 sylancom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ 𝑧 ) ∈ 𝐵 )
90 88 38 sylancom ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) = 𝑧 )
91 90 eqcomd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 = ( ⊥ ‘ ( ⊥ ‘ 𝑧 ) ) )
92 89 91 42 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ∃ 𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘ 𝑢 ) )
93 breq2 ⊢ ( 𝑧 = ( ⊥ ‘ 𝑢 ) → ( ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) )
94 44 93 imbi12d ⊢ ( 𝑧 = ( ⊥ ‘ 𝑢 ) → ( ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
95 94 adantl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) ∧ 𝑧 = ( ⊥ ‘ 𝑢 ) ) → ( ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
96 87 92 95 ralxfrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑢 ) ) ) )
97 86 96 bitr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑡 ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) ) )
98 59 ralrab ⊢ ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 ↔ ∀ 𝑢 ∈ 𝐵 ( ( ⊥ ‘ 𝑢 ) ∈ 𝑆 → 𝑢 ( le ‘ 𝐾 ) 𝑡 ) )
99 56 ralrab ⊢ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑧 ∈ 𝑆 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) )
100 97 98 99 3bitr4g ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 ↔ ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 ) )
101 simplr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → 𝑣 ∈ 𝐵 )
102 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → 𝑡 ∈ 𝐵 )
103 1 10 4 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑣 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵 ) → ( 𝑣 ( le ‘ 𝐾 ) 𝑡 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) )
104 62 101 102 103 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( 𝑣 ( le ‘ 𝐾 ) 𝑡 ↔ ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) )
105 100 104 imbi12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) ∧ 𝑡 ∈ 𝐵 ) → ( ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ↔ ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
106 105 ralbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ↔ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) 𝑧 → ( ⊥ ‘ 𝑡 ) ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) )
107 79 106 bitr4d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ↔ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) )
108 61 107 anbi12d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵 ) → ( ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ↔ ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) ) )
109 108 riotabidva ⊢ ( 𝐾 ∈ HL → ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) = ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) ) )
110 ssrab2 ⊢ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ⊆ 𝐵
111 biid ⊢ ( ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) ↔ ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) )
112 simpl ⊢ ( ( 𝐾 ∈ HL ∧ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ⊆ 𝐵 ) → 𝐾 ∈ HL )
113 simpr ⊢ ( ( 𝐾 ∈ HL ∧ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ⊆ 𝐵 ) → { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ⊆ 𝐵 )
114 1 10 2 111 112 113 lubval ⊢ ( ( 𝐾 ∈ HL ∧ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ⊆ 𝐵 ) → ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) = ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) ) )
115 110 114 mpan2 ⊢ ( 𝐾 ∈ HL → ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) = ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑣 ∧ ∀ 𝑡 ∈ 𝐵 ( ∀ 𝑢 ∈ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } 𝑢 ( le ‘ 𝐾 ) 𝑡 → 𝑣 ( le ‘ 𝐾 ) 𝑡 ) ) ) )
116 109 115 eqtr4d ⊢ ( 𝐾 ∈ HL → ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) = ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) )
117 116 fveq2d ⊢ ( 𝐾 ∈ HL → ( ⊥ ‘ ( ℩ 𝑣 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ( ⊥ ‘ 𝑣 ) ( le ‘ 𝐾 ) 𝑧 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } 𝑤 ( le ‘ 𝐾 ) 𝑧 → 𝑤 ( le ‘ 𝐾 ) ( ⊥ ‘ 𝑣 ) ) ) ) ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) ) )
118 15 31 117 3eqtrd ⊢ ( 𝐾 ∈ HL → ( 𝐺 ‘ { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) ) )
119 9 118 sylan9eqr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑆 ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑥 ) ∈ 𝑆 } ) ) )