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

Theorem glbconN 33681
 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.)
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 dfin5 3548 . . . 4 (𝐵𝑆) = {𝑥𝐵𝑥𝑆}
2 sseqin2 3779 . . . . 5 (𝑆𝐵 ↔ (𝐵𝑆) = 𝑆)
32biimpi 205 . . . 4 (𝑆𝐵 → (𝐵𝑆) = 𝑆)
41, 3syl5reqr 2659 . . 3 (𝑆𝐵𝑆 = {𝑥𝐵𝑥𝑆})
54fveq2d 6107 . 2 (𝑆𝐵 → (𝐺𝑆) = (𝐺‘{𝑥𝐵𝑥𝑆}))
6 glbcon.b . . . 4 𝐵 = (Base‘𝐾)
7 eqid 2610 . . . 4 (le‘𝐾) = (le‘𝐾)
8 glbcon.g . . . 4 𝐺 = (glb‘𝐾)
9 biid 250 . . . 4 ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)))
10 id 22 . . . 4 (𝐾 ∈ HL → 𝐾 ∈ HL)
11 ssrab2 3650 . . . . 5 {𝑥𝐵𝑥𝑆} ⊆ 𝐵
1211a1i 11 . . . 4 (𝐾 ∈ HL → {𝑥𝐵𝑥𝑆} ⊆ 𝐵)
136, 7, 8, 9, 10, 12glbval 16820 . . 3 (𝐾 ∈ HL → (𝐺‘{𝑥𝐵𝑥𝑆}) = (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))))
14 hlop 33667 . . . 4 (𝐾 ∈ HL → 𝐾 ∈ OP)
15 hlclat 33663 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ CLat)
166, 8clatglbcl 16937 . . . . . . 7 ((𝐾 ∈ CLat ∧ {𝑥𝐵𝑥𝑆} ⊆ 𝐵) → (𝐺‘{𝑥𝐵𝑥𝑆}) ∈ 𝐵)
1715, 11, 16sylancl 693 . . . . . 6 (𝐾 ∈ HL → (𝐺‘{𝑥𝐵𝑥𝑆}) ∈ 𝐵)
1813, 17eqeltrrd 2689 . . . . 5 (𝐾 ∈ HL → (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) ∈ 𝐵)
19 fvex 6113 . . . . . . 7 (Base‘𝐾) ∈ V
206, 19eqeltri 2684 . . . . . 6 𝐵 ∈ V
2120riotaclbBAD 33259 . . . . 5 (∃!𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)) ↔ (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) ∈ 𝐵)
2218, 21sylibr 223 . . . 4 (𝐾 ∈ HL → ∃!𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)))
23 glbcon.o . . . . 5 = (oc‘𝐾)
24 breq1 4586 . . . . . . 7 (𝑦 = ( 𝑣) → (𝑦(le‘𝐾)𝑧 ↔ ( 𝑣)(le‘𝐾)𝑧))
2524ralbidv 2969 . . . . . 6 (𝑦 = ( 𝑣) → (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧))
26 breq2 4587 . . . . . . . 8 (𝑦 = ( 𝑣) → (𝑤(le‘𝐾)𝑦𝑤(le‘𝐾)( 𝑣)))
2726imbi2d 329 . . . . . . 7 (𝑦 = ( 𝑣) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))
2827ralbidv 2969 . . . . . 6 (𝑦 = ( 𝑣) → (∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦) ↔ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))
2925, 28anbi12d 743 . . . . 5 (𝑦 = ( 𝑣) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)))))
306, 23, 29riotaocN 33514 . . . 4 ((𝐾 ∈ OP ∧ ∃!𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) → (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) = ( ‘(𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))))
3114, 22, 30syl2anc 691 . . 3 (𝐾 ∈ HL → (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) = ( ‘(𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))))
3214ad2antrr 758 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → 𝐾 ∈ OP)
336, 23opoccl 33499 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑢𝐵) → ( 𝑢) ∈ 𝐵)
3432, 33sylancom 698 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → ( 𝑢) ∈ 𝐵)
3514ad2antrr 758 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → 𝐾 ∈ OP)
366, 23opoccl 33499 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑧𝐵) → ( 𝑧) ∈ 𝐵)
3735, 36sylancom 698 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → ( 𝑧) ∈ 𝐵)
386, 23opococ 33500 . . . . . . . . . . . . 13 ((𝐾 ∈ OP ∧ 𝑧𝐵) → ( ‘( 𝑧)) = 𝑧)
3935, 38sylancom 698 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → ( ‘( 𝑧)) = 𝑧)
4039eqcomd 2616 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → 𝑧 = ( ‘( 𝑧)))
41 fveq2 6103 . . . . . . . . . . . . 13 (𝑢 = ( 𝑧) → ( 𝑢) = ( ‘( 𝑧)))
4241eqeq2d 2620 . . . . . . . . . . . 12 (𝑢 = ( 𝑧) → (𝑧 = ( 𝑢) ↔ 𝑧 = ( ‘( 𝑧))))
4342rspcev 3282 . . . . . . . . . . 11 ((( 𝑧) ∈ 𝐵𝑧 = ( ‘( 𝑧))) → ∃𝑢𝐵 𝑧 = ( 𝑢))
4437, 40, 43syl2anc 691 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → ∃𝑢𝐵 𝑧 = ( 𝑢))
45 eleq1 2676 . . . . . . . . . . . 12 (𝑧 = ( 𝑢) → (𝑧𝑆 ↔ ( 𝑢) ∈ 𝑆))
46 breq2 4587 . . . . . . . . . . . 12 (𝑧 = ( 𝑢) → (( 𝑣)(le‘𝐾)𝑧 ↔ ( 𝑣)(le‘𝐾)( 𝑢)))
4745, 46imbi12d 333 . . . . . . . . . . 11 (𝑧 = ( 𝑢) → ((𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
4847adantl 481 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧 = ( 𝑢)) → ((𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
4934, 44, 48ralxfrd 4805 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑧𝐵 (𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
50 simpr 476 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → 𝑢𝐵)
51 simplr 788 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → 𝑣𝐵)
526, 7, 23oplecon3b 33505 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑢𝐵𝑣𝐵) → (𝑢(le‘𝐾)𝑣 ↔ ( 𝑣)(le‘𝐾)( 𝑢)))
5332, 50, 51, 52syl3anc 1318 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → (𝑢(le‘𝐾)𝑣 ↔ ( 𝑣)(le‘𝐾)( 𝑢)))
5453imbi2d 329 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → ((( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
5554ralbidva 2968 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
5649, 55bitr4d 270 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑧𝐵 (𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣)))
57 eleq1 2676 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥𝑆𝑧𝑆))
5857ralrab 3335 . . . . . . . 8 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ↔ ∀𝑧𝐵 (𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧))
59 fveq2 6103 . . . . . . . . . 10 (𝑥 = 𝑢 → ( 𝑥) = ( 𝑢))
6059eleq1d 2672 . . . . . . . . 9 (𝑥 = 𝑢 → (( 𝑥) ∈ 𝑆 ↔ ( 𝑢) ∈ 𝑆))
6160ralrab 3335 . . . . . . . 8 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣))
6256, 58, 613bitr4g 302 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ↔ ∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣))
6314ad2antrr 758 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → 𝐾 ∈ OP)
646, 23opoccl 33499 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑡𝐵) → ( 𝑡) ∈ 𝐵)
6563, 64sylancom 698 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → ( 𝑡) ∈ 𝐵)
6614ad2antrr 758 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → 𝐾 ∈ OP)
676, 23opoccl 33499 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑤𝐵) → ( 𝑤) ∈ 𝐵)
6866, 67sylancom 698 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → ( 𝑤) ∈ 𝐵)
696, 23opococ 33500 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑤𝐵) → ( ‘( 𝑤)) = 𝑤)
7066, 69sylancom 698 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → ( ‘( 𝑤)) = 𝑤)
7170eqcomd 2616 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → 𝑤 = ( ‘( 𝑤)))
72 fveq2 6103 . . . . . . . . . . . 12 (𝑡 = ( 𝑤) → ( 𝑡) = ( ‘( 𝑤)))
7372eqeq2d 2620 . . . . . . . . . . 11 (𝑡 = ( 𝑤) → (𝑤 = ( 𝑡) ↔ 𝑤 = ( ‘( 𝑤))))
7473rspcev 3282 . . . . . . . . . 10 ((( 𝑤) ∈ 𝐵𝑤 = ( ‘( 𝑤))) → ∃𝑡𝐵 𝑤 = ( 𝑡))
7568, 71, 74syl2anc 691 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → ∃𝑡𝐵 𝑤 = ( 𝑡))
76 breq1 4586 . . . . . . . . . . . 12 (𝑤 = ( 𝑡) → (𝑤(le‘𝐾)𝑧 ↔ ( 𝑡)(le‘𝐾)𝑧))
7776ralbidv 2969 . . . . . . . . . . 11 (𝑤 = ( 𝑡) → (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧))
78 breq1 4586 . . . . . . . . . . 11 (𝑤 = ( 𝑡) → (𝑤(le‘𝐾)( 𝑣) ↔ ( 𝑡)(le‘𝐾)( 𝑣)))
7977, 78imbi12d 333 . . . . . . . . . 10 (𝑤 = ( 𝑡) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
8079adantl 481 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤 = ( 𝑡)) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
8165, 75, 80ralxfrd 4805 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ ∀𝑡𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
8214ad3antrrr 762 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → 𝐾 ∈ OP)
83 simpr 476 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → 𝑢𝐵)
84 simplr 788 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → 𝑡𝐵)
856, 7, 23oplecon3b 33505 . . . . . . . . . . . . . . 15 ((𝐾 ∈ OP ∧ 𝑢𝐵𝑡𝐵) → (𝑢(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑢)))
8682, 83, 84, 85syl3anc 1318 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → (𝑢(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑢)))
8786imbi2d 329 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → ((( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
8887ralbidva 2968 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
8982, 33sylancom 698 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → ( 𝑢) ∈ 𝐵)
9014ad3antrrr 762 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → 𝐾 ∈ OP)
9190, 36sylancom 698 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → ( 𝑧) ∈ 𝐵)
9290, 38sylancom 698 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → ( ‘( 𝑧)) = 𝑧)
9392eqcomd 2616 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → 𝑧 = ( ‘( 𝑧)))
9491, 93, 43syl2anc 691 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → ∃𝑢𝐵 𝑧 = ( 𝑢))
95 breq2 4587 . . . . . . . . . . . . . . 15 (𝑧 = ( 𝑢) → (( 𝑡)(le‘𝐾)𝑧 ↔ ( 𝑡)(le‘𝐾)( 𝑢)))
9645, 95imbi12d 333 . . . . . . . . . . . . . 14 (𝑧 = ( 𝑢) → ((𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
9796adantl 481 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧 = ( 𝑢)) → ((𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
9889, 94, 97ralxfrd 4805 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑧𝐵 (𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
9988, 98bitr4d 270 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡) ↔ ∀𝑧𝐵 (𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧)))
10060ralrab 3335 . . . . . . . . . . 11 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡))
10157ralrab 3335 . . . . . . . . . . 11 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 ↔ ∀𝑧𝐵 (𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧))
10299, 100, 1013bitr4g 302 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 ↔ ∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧))
103 simplr 788 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → 𝑣𝐵)
104 simpr 476 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → 𝑡𝐵)
1056, 7, 23oplecon3b 33505 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑣𝐵𝑡𝐵) → (𝑣(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑣)))
10663, 103, 104, 105syl3anc 1318 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (𝑣(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑣)))
107102, 106imbi12d 333 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → ((∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
108107ralbidva 2968 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡) ↔ ∀𝑡𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
10981, 108bitr4d 270 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡)))
11062, 109anbi12d 743 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑣𝐵) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))) ↔ (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
111110riotabidva 6527 . . . . 5 (𝐾 ∈ HL → (𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)))) = (𝑣𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
112 ssrab2 3650 . . . . . 6 {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵
113 glbcon.u . . . . . . 7 𝑈 = (lub‘𝐾)
114 biid 250 . . . . . . 7 ((∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡)) ↔ (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡)))
115 simpl 472 . . . . . . 7 ((𝐾 ∈ HL ∧ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵) → 𝐾 ∈ HL)
116 simpr 476 . . . . . . 7 ((𝐾 ∈ HL ∧ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵) → {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵)
1176, 7, 113, 114, 115, 116lubval 16807 . . . . . 6 ((𝐾 ∈ HL ∧ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵) → (𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}) = (𝑣𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
118112, 117mpan2 703 . . . . 5 (𝐾 ∈ HL → (𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}) = (𝑣𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
119111, 118eqtr4d 2647 . . . 4 (𝐾 ∈ HL → (𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)))) = (𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}))
120119fveq2d 6107 . . 3 (𝐾 ∈ HL → ( ‘(𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))) = ( ‘(𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆})))
12113, 31, 1203eqtrd 2648 . 2 (𝐾 ∈ HL → (𝐺‘{𝑥𝐵𝑥𝑆}) = ( ‘(𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆})))
1225, 121sylan9eqr 2666 1 ((𝐾 ∈ HL ∧ 𝑆𝐵) → (𝐺𝑆) = ( ‘(𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆})))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  {crab 2900  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540   class class class wbr 4583  ‘cfv 5804  ℩crio 6510  Basecbs 15695  lecple 15775  occoc 15776  lubclub 16765  glbcglb 16766  CLatccla 16930  OPcops 33477  HLchlt 33655 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-riotaBAD 33257 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-undef 7286  df-lub 16797  df-glb 16798  df-clat 16931  df-oposet 33481  df-ol 33483  df-oml 33484  df-hlat 33656 This theorem is referenced by:  glbconxN  33682
 Copyright terms: Public domain W3C validator