Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  glbconN Structured version   Visualization version   GIF version

Theorem glbconN 38247
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 7365. (Revised by SN, 3-Jan-2025.) (New usage is discouraged.)
Hypotheses
Ref Expression
glbcon.b 𝐡 = (Baseβ€˜πΎ)
glbcon.u π‘ˆ = (lubβ€˜πΎ)
glbcon.g 𝐺 = (glbβ€˜πΎ)
glbcon.o βŠ₯ = (ocβ€˜πΎ)
Assertion
Ref Expression
glbconN ((𝐾 ∈ HL ∧ 𝑆 βŠ† 𝐡) β†’ (πΊβ€˜π‘†) = ( βŠ₯ β€˜(π‘ˆβ€˜{π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆})))
Distinct variable groups:   π‘₯,𝐡   π‘₯, βŠ₯   π‘₯,𝑆
Allowed substitution hints:   π‘ˆ(π‘₯)   𝐺(π‘₯)   𝐾(π‘₯)

Proof of Theorem glbconN
Dummy variables 𝑒 𝑑 𝑣 𝑀 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseqin2 4216 . . . . 5 (𝑆 βŠ† 𝐡 ↔ (𝐡 ∩ 𝑆) = 𝑆)
21biimpi 215 . . . 4 (𝑆 βŠ† 𝐡 β†’ (𝐡 ∩ 𝑆) = 𝑆)
3 dfin5 3957 . . . 4 (𝐡 ∩ 𝑆) = {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}
42, 3eqtr3di 2788 . . 3 (𝑆 βŠ† 𝐡 β†’ 𝑆 = {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆})
54fveq2d 6896 . 2 (𝑆 βŠ† 𝐡 β†’ (πΊβ€˜π‘†) = (πΊβ€˜{π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}))
6 glbcon.b . . . 4 𝐡 = (Baseβ€˜πΎ)
7 eqid 2733 . . . 4 (leβ€˜πΎ) = (leβ€˜πΎ)
8 glbcon.g . . . 4 𝐺 = (glbβ€˜πΎ)
9 biid 261 . . . 4 ((βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)𝑦)) ↔ (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)𝑦)))
10 id 22 . . . 4 (𝐾 ∈ HL β†’ 𝐾 ∈ HL)
11 ssrab2 4078 . . . . 5 {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} βŠ† 𝐡
1211a1i 11 . . . 4 (𝐾 ∈ HL β†’ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} βŠ† 𝐡)
136, 7, 8, 9, 10, 12glbval 18322 . . 3 (𝐾 ∈ HL β†’ (πΊβ€˜{π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}) = (℩𝑦 ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)𝑦))))
14 hlop 38232 . . . 4 (𝐾 ∈ HL β†’ 𝐾 ∈ OP)
15 hlclat 38228 . . . . . 6 (𝐾 ∈ HL β†’ 𝐾 ∈ CLat)
166, 8clatglbcl2 18459 . . . . . 6 ((𝐾 ∈ CLat ∧ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} βŠ† 𝐡) β†’ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ∈ dom 𝐺)
1715, 12, 16syl2anc 585 . . . . 5 (𝐾 ∈ HL β†’ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ∈ dom 𝐺)
186, 7, 8, 9, 10, 17glbeu 18321 . . . 4 (𝐾 ∈ HL β†’ βˆƒ!𝑦 ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)𝑦)))
19 glbcon.o . . . . 5 βŠ₯ = (ocβ€˜πΎ)
20 breq1 5152 . . . . . . 7 (𝑦 = ( βŠ₯ β€˜π‘£) β†’ (𝑦(leβ€˜πΎ)𝑧 ↔ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧))
2120ralbidv 3178 . . . . . 6 (𝑦 = ( βŠ₯ β€˜π‘£) β†’ (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑦(leβ€˜πΎ)𝑧 ↔ βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧))
22 breq2 5153 . . . . . . . 8 (𝑦 = ( βŠ₯ β€˜π‘£) β†’ (𝑀(leβ€˜πΎ)𝑦 ↔ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£)))
2322imbi2d 341 . . . . . . 7 (𝑦 = ( βŠ₯ β€˜π‘£) β†’ ((βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)𝑦) ↔ (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£))))
2423ralbidv 3178 . . . . . 6 (𝑦 = ( βŠ₯ β€˜π‘£) β†’ (βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)𝑦) ↔ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£))))
2521, 24anbi12d 632 . . . . 5 (𝑦 = ( βŠ₯ β€˜π‘£) β†’ ((βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)𝑦)) ↔ (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£)))))
266, 19, 25riotaocN 38079 . . . 4 ((𝐾 ∈ OP ∧ βˆƒ!𝑦 ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)𝑦))) β†’ (℩𝑦 ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)𝑦))) = ( βŠ₯ β€˜(℩𝑣 ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£))))))
2714, 18, 26syl2anc 585 . . 3 (𝐾 ∈ HL β†’ (℩𝑦 ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑦(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)𝑦))) = ( βŠ₯ β€˜(℩𝑣 ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£))))))
2814ad2antrr 725 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ 𝐾 ∈ OP)
296, 19opoccl 38064 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑒 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘’) ∈ 𝐡)
3028, 29sylancom 589 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘’) ∈ 𝐡)
3114ad2antrr 725 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝐾 ∈ OP)
326, 19opoccl 38064 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑧 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘§) ∈ 𝐡)
3331, 32sylancom 589 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘§) ∈ 𝐡)
346, 19opococ 38065 . . . . . . . . . . . . 13 ((𝐾 ∈ OP ∧ 𝑧 ∈ 𝐡) β†’ ( βŠ₯ β€˜( βŠ₯ β€˜π‘§)) = 𝑧)
3531, 34sylancom 589 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ ( βŠ₯ β€˜( βŠ₯ β€˜π‘§)) = 𝑧)
3635eqcomd 2739 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 = ( βŠ₯ β€˜( βŠ₯ β€˜π‘§)))
37 fveq2 6892 . . . . . . . . . . . 12 (𝑒 = ( βŠ₯ β€˜π‘§) β†’ ( βŠ₯ β€˜π‘’) = ( βŠ₯ β€˜( βŠ₯ β€˜π‘§)))
3837rspceeqv 3634 . . . . . . . . . . 11 ((( βŠ₯ β€˜π‘§) ∈ 𝐡 ∧ 𝑧 = ( βŠ₯ β€˜( βŠ₯ β€˜π‘§))) β†’ βˆƒπ‘’ ∈ 𝐡 𝑧 = ( βŠ₯ β€˜π‘’))
3933, 36, 38syl2anc 585 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ βˆƒπ‘’ ∈ 𝐡 𝑧 = ( βŠ₯ β€˜π‘’))
40 eleq1 2822 . . . . . . . . . . . 12 (𝑧 = ( βŠ₯ β€˜π‘’) β†’ (𝑧 ∈ 𝑆 ↔ ( βŠ₯ β€˜π‘’) ∈ 𝑆))
41 breq2 5153 . . . . . . . . . . . 12 (𝑧 = ( βŠ₯ β€˜π‘’) β†’ (( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧 ↔ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)( βŠ₯ β€˜π‘’)))
4240, 41imbi12d 345 . . . . . . . . . . 11 (𝑧 = ( βŠ₯ β€˜π‘’) β†’ ((𝑧 ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧) ↔ (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)( βŠ₯ β€˜π‘’))))
4342adantl 483 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑧 = ( βŠ₯ β€˜π‘’)) β†’ ((𝑧 ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧) ↔ (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)( βŠ₯ β€˜π‘’))))
4430, 39, 43ralxfrd 5407 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) β†’ (βˆ€π‘§ ∈ 𝐡 (𝑧 ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧) ↔ βˆ€π‘’ ∈ 𝐡 (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)( βŠ₯ β€˜π‘’))))
45 simpr 486 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ 𝑒 ∈ 𝐡)
46 simplr 768 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ 𝑣 ∈ 𝐡)
476, 7, 19oplecon3b 38070 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑒 ∈ 𝐡 ∧ 𝑣 ∈ 𝐡) β†’ (𝑒(leβ€˜πΎ)𝑣 ↔ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)( βŠ₯ β€˜π‘’)))
4828, 45, 46, 47syl3anc 1372 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ (𝑒(leβ€˜πΎ)𝑣 ↔ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)( βŠ₯ β€˜π‘’)))
4948imbi2d 341 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ ((( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ 𝑒(leβ€˜πΎ)𝑣) ↔ (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)( βŠ₯ β€˜π‘’))))
5049ralbidva 3176 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) β†’ (βˆ€π‘’ ∈ 𝐡 (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ 𝑒(leβ€˜πΎ)𝑣) ↔ βˆ€π‘’ ∈ 𝐡 (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)( βŠ₯ β€˜π‘’))))
5144, 50bitr4d 282 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) β†’ (βˆ€π‘§ ∈ 𝐡 (𝑧 ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧) ↔ βˆ€π‘’ ∈ 𝐡 (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ 𝑒(leβ€˜πΎ)𝑣)))
52 eleq1 2822 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (π‘₯ ∈ 𝑆 ↔ 𝑧 ∈ 𝑆))
5352ralrab 3690 . . . . . . . 8 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧 ↔ βˆ€π‘§ ∈ 𝐡 (𝑧 ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧))
54 fveq2 6892 . . . . . . . . . 10 (π‘₯ = 𝑒 β†’ ( βŠ₯ β€˜π‘₯) = ( βŠ₯ β€˜π‘’))
5554eleq1d 2819 . . . . . . . . 9 (π‘₯ = 𝑒 β†’ (( βŠ₯ β€˜π‘₯) ∈ 𝑆 ↔ ( βŠ₯ β€˜π‘’) ∈ 𝑆))
5655ralrab 3690 . . . . . . . 8 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑣 ↔ βˆ€π‘’ ∈ 𝐡 (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ 𝑒(leβ€˜πΎ)𝑣))
5751, 53, 563bitr4g 314 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) β†’ (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧 ↔ βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑣))
5814ad2antrr 725 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ 𝐾 ∈ OP)
596, 19opoccl 38064 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑑 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘‘) ∈ 𝐡)
6058, 59sylancom 589 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘‘) ∈ 𝐡)
6114ad2antrr 725 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑀 ∈ 𝐡) β†’ 𝐾 ∈ OP)
626, 19opoccl 38064 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑀 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘€) ∈ 𝐡)
6361, 62sylancom 589 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑀 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘€) ∈ 𝐡)
646, 19opococ 38065 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑀 ∈ 𝐡) β†’ ( βŠ₯ β€˜( βŠ₯ β€˜π‘€)) = 𝑀)
6561, 64sylancom 589 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑀 ∈ 𝐡) β†’ ( βŠ₯ β€˜( βŠ₯ β€˜π‘€)) = 𝑀)
6665eqcomd 2739 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑀 ∈ 𝐡) β†’ 𝑀 = ( βŠ₯ β€˜( βŠ₯ β€˜π‘€)))
67 fveq2 6892 . . . . . . . . . . 11 (𝑑 = ( βŠ₯ β€˜π‘€) β†’ ( βŠ₯ β€˜π‘‘) = ( βŠ₯ β€˜( βŠ₯ β€˜π‘€)))
6867rspceeqv 3634 . . . . . . . . . 10 ((( βŠ₯ β€˜π‘€) ∈ 𝐡 ∧ 𝑀 = ( βŠ₯ β€˜( βŠ₯ β€˜π‘€))) β†’ βˆƒπ‘‘ ∈ 𝐡 𝑀 = ( βŠ₯ β€˜π‘‘))
6963, 66, 68syl2anc 585 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑀 ∈ 𝐡) β†’ βˆƒπ‘‘ ∈ 𝐡 𝑀 = ( βŠ₯ β€˜π‘‘))
70 breq1 5152 . . . . . . . . . . . 12 (𝑀 = ( βŠ₯ β€˜π‘‘) β†’ (𝑀(leβ€˜πΎ)𝑧 ↔ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧))
7170ralbidv 3178 . . . . . . . . . . 11 (𝑀 = ( βŠ₯ β€˜π‘‘) β†’ (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 ↔ βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧))
72 breq1 5152 . . . . . . . . . . 11 (𝑀 = ( βŠ₯ β€˜π‘‘) β†’ (𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£) ↔ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘£)))
7371, 72imbi12d 345 . . . . . . . . . 10 (𝑀 = ( βŠ₯ β€˜π‘‘) β†’ ((βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£)) ↔ (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘£))))
7473adantl 483 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑀 = ( βŠ₯ β€˜π‘‘)) β†’ ((βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£)) ↔ (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘£))))
7560, 69, 74ralxfrd 5407 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) β†’ (βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£)) ↔ βˆ€π‘‘ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘£))))
7614ad3antrrr 729 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ 𝐾 ∈ OP)
77 simpr 486 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ 𝑒 ∈ 𝐡)
78 simplr 768 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ 𝑑 ∈ 𝐡)
796, 7, 19oplecon3b 38070 . . . . . . . . . . . . . . 15 ((𝐾 ∈ OP ∧ 𝑒 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡) β†’ (𝑒(leβ€˜πΎ)𝑑 ↔ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘’)))
8076, 77, 78, 79syl3anc 1372 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ (𝑒(leβ€˜πΎ)𝑑 ↔ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘’)))
8180imbi2d 341 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ ((( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ 𝑒(leβ€˜πΎ)𝑑) ↔ (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘’))))
8281ralbidva 3176 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ (βˆ€π‘’ ∈ 𝐡 (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ 𝑒(leβ€˜πΎ)𝑑) ↔ βˆ€π‘’ ∈ 𝐡 (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘’))))
8376, 29sylancom 589 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑒 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘’) ∈ 𝐡)
8414ad3antrrr 729 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝐾 ∈ OP)
8584, 32sylancom 589 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ ( βŠ₯ β€˜π‘§) ∈ 𝐡)
8684, 34sylancom 589 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ ( βŠ₯ β€˜( βŠ₯ β€˜π‘§)) = 𝑧)
8786eqcomd 2739 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ 𝑧 = ( βŠ₯ β€˜( βŠ₯ β€˜π‘§)))
8885, 87, 38syl2anc 585 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑧 ∈ 𝐡) β†’ βˆƒπ‘’ ∈ 𝐡 𝑧 = ( βŠ₯ β€˜π‘’))
89 breq2 5153 . . . . . . . . . . . . . . 15 (𝑧 = ( βŠ₯ β€˜π‘’) β†’ (( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧 ↔ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘’)))
9040, 89imbi12d 345 . . . . . . . . . . . . . 14 (𝑧 = ( βŠ₯ β€˜π‘’) β†’ ((𝑧 ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧) ↔ (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘’))))
9190adantl 483 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑧 = ( βŠ₯ β€˜π‘’)) β†’ ((𝑧 ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧) ↔ (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘’))))
9283, 88, 91ralxfrd 5407 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ (βˆ€π‘§ ∈ 𝐡 (𝑧 ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧) ↔ βˆ€π‘’ ∈ 𝐡 (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘’))))
9382, 92bitr4d 282 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ (βˆ€π‘’ ∈ 𝐡 (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ 𝑒(leβ€˜πΎ)𝑑) ↔ βˆ€π‘§ ∈ 𝐡 (𝑧 ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧)))
9455ralrab 3690 . . . . . . . . . . 11 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 ↔ βˆ€π‘’ ∈ 𝐡 (( βŠ₯ β€˜π‘’) ∈ 𝑆 β†’ 𝑒(leβ€˜πΎ)𝑑))
9552ralrab 3690 . . . . . . . . . . 11 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧 ↔ βˆ€π‘§ ∈ 𝐡 (𝑧 ∈ 𝑆 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧))
9693, 94, 953bitr4g 314 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 ↔ βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧))
97 simplr 768 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ 𝑣 ∈ 𝐡)
98 simpr 486 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ 𝑑 ∈ 𝐡)
996, 7, 19oplecon3b 38070 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑣 ∈ 𝐡 ∧ 𝑑 ∈ 𝐡) β†’ (𝑣(leβ€˜πΎ)𝑑 ↔ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘£)))
10058, 97, 98, 99syl3anc 1372 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ (𝑣(leβ€˜πΎ)𝑑 ↔ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘£)))
10196, 100imbi12d 345 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ ((βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 β†’ 𝑣(leβ€˜πΎ)𝑑) ↔ (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘£))))
102101ralbidva 3176 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) β†’ (βˆ€π‘‘ ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 β†’ 𝑣(leβ€˜πΎ)𝑑) ↔ βˆ€π‘‘ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)𝑧 β†’ ( βŠ₯ β€˜π‘‘)(leβ€˜πΎ)( βŠ₯ β€˜π‘£))))
10375, 102bitr4d 282 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) β†’ (βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£)) ↔ βˆ€π‘‘ ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 β†’ 𝑣(leβ€˜πΎ)𝑑)))
10457, 103anbi12d 632 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐡) β†’ ((βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£))) ↔ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑣 ∧ βˆ€π‘‘ ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 β†’ 𝑣(leβ€˜πΎ)𝑑))))
105104riotabidva 7385 . . . . 5 (𝐾 ∈ HL β†’ (℩𝑣 ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£)))) = (℩𝑣 ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑣 ∧ βˆ€π‘‘ ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 β†’ 𝑣(leβ€˜πΎ)𝑑))))
106 ssrab2 4078 . . . . . 6 {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆} βŠ† 𝐡
107 glbcon.u . . . . . . 7 π‘ˆ = (lubβ€˜πΎ)
108 biid 261 . . . . . . 7 ((βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑣 ∧ βˆ€π‘‘ ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 β†’ 𝑣(leβ€˜πΎ)𝑑)) ↔ (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑣 ∧ βˆ€π‘‘ ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 β†’ 𝑣(leβ€˜πΎ)𝑑)))
109 simpl 484 . . . . . . 7 ((𝐾 ∈ HL ∧ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆} βŠ† 𝐡) β†’ 𝐾 ∈ HL)
110 simpr 486 . . . . . . 7 ((𝐾 ∈ HL ∧ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆} βŠ† 𝐡) β†’ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆} βŠ† 𝐡)
1116, 7, 107, 108, 109, 110lubval 18309 . . . . . 6 ((𝐾 ∈ HL ∧ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆} βŠ† 𝐡) β†’ (π‘ˆβ€˜{π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}) = (℩𝑣 ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑣 ∧ βˆ€π‘‘ ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 β†’ 𝑣(leβ€˜πΎ)𝑑))))
112106, 111mpan2 690 . . . . 5 (𝐾 ∈ HL β†’ (π‘ˆβ€˜{π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}) = (℩𝑣 ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑣 ∧ βˆ€π‘‘ ∈ 𝐡 (βˆ€π‘’ ∈ {π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}𝑒(leβ€˜πΎ)𝑑 β†’ 𝑣(leβ€˜πΎ)𝑑))))
113105, 112eqtr4d 2776 . . . 4 (𝐾 ∈ HL β†’ (℩𝑣 ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£)))) = (π‘ˆβ€˜{π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆}))
114113fveq2d 6896 . . 3 (𝐾 ∈ HL β†’ ( βŠ₯ β€˜(℩𝑣 ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆} ( βŠ₯ β€˜π‘£)(leβ€˜πΎ)𝑧 ∧ βˆ€π‘€ ∈ 𝐡 (βˆ€π‘§ ∈ {π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}𝑀(leβ€˜πΎ)𝑧 β†’ 𝑀(leβ€˜πΎ)( βŠ₯ β€˜π‘£))))) = ( βŠ₯ β€˜(π‘ˆβ€˜{π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆})))
11513, 27, 1143eqtrd 2777 . 2 (𝐾 ∈ HL β†’ (πΊβ€˜{π‘₯ ∈ 𝐡 ∣ π‘₯ ∈ 𝑆}) = ( βŠ₯ β€˜(π‘ˆβ€˜{π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆})))
1165, 115sylan9eqr 2795 1 ((𝐾 ∈ HL ∧ 𝑆 βŠ† 𝐡) β†’ (πΊβ€˜π‘†) = ( βŠ₯ β€˜(π‘ˆβ€˜{π‘₯ ∈ 𝐡 ∣ ( βŠ₯ β€˜π‘₯) ∈ 𝑆})))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  βˆƒwrex 3071  βˆƒ!wreu 3375  {crab 3433   ∩ cin 3948   βŠ† wss 3949   class class class wbr 5149  dom cdm 5677  β€˜cfv 6544  β„©crio 7364  Basecbs 17144  lecple 17204  occoc 17205  lubclub 18262  glbcglb 18263  CLatccla 18451  OPcops 38042  HLchlt 38220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-lub 18299  df-glb 18300  df-clat 18452  df-oposet 38046  df-ol 38048  df-oml 38049  df-hlat 38221
This theorem is referenced by:  glbconxN  38249
  Copyright terms: Public domain W3C validator