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 35540
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 3800 . . . 4 (𝐵𝑆) = {𝑥𝐵𝑥𝑆}
2 sseqin2 4040 . . . . 5 (𝑆𝐵 ↔ (𝐵𝑆) = 𝑆)
32biimpi 208 . . . 4 (𝑆𝐵 → (𝐵𝑆) = 𝑆)
41, 3syl5reqr 2829 . . 3 (𝑆𝐵𝑆 = {𝑥𝐵𝑥𝑆})
54fveq2d 6452 . 2 (𝑆𝐵 → (𝐺𝑆) = (𝐺‘{𝑥𝐵𝑥𝑆}))
6 glbcon.b . . . 4 𝐵 = (Base‘𝐾)
7 eqid 2778 . . . 4 (le‘𝐾) = (le‘𝐾)
8 glbcon.g . . . 4 𝐺 = (glb‘𝐾)
9 biid 253 . . . 4 ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)))
10 id 22 . . . 4 (𝐾 ∈ HL → 𝐾 ∈ HL)
11 ssrab2 3908 . . . . 5 {𝑥𝐵𝑥𝑆} ⊆ 𝐵
1211a1i 11 . . . 4 (𝐾 ∈ HL → {𝑥𝐵𝑥𝑆} ⊆ 𝐵)
136, 7, 8, 9, 10, 12glbval 17394 . . 3 (𝐾 ∈ HL → (𝐺‘{𝑥𝐵𝑥𝑆}) = (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))))
14 hlop 35525 . . . 4 (𝐾 ∈ HL → 𝐾 ∈ OP)
15 hlclat 35521 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ CLat)
166, 8clatglbcl 17511 . . . . . . 7 ((𝐾 ∈ CLat ∧ {𝑥𝐵𝑥𝑆} ⊆ 𝐵) → (𝐺‘{𝑥𝐵𝑥𝑆}) ∈ 𝐵)
1715, 11, 16sylancl 580 . . . . . 6 (𝐾 ∈ HL → (𝐺‘{𝑥𝐵𝑥𝑆}) ∈ 𝐵)
1813, 17eqeltrrd 2860 . . . . 5 (𝐾 ∈ HL → (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) ∈ 𝐵)
196fvexi 6462 . . . . . 6 𝐵 ∈ V
2019riotaclbBAD 35118 . . . . 5 (∃!𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)) ↔ (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) ∈ 𝐵)
2118, 20sylibr 226 . . . 4 (𝐾 ∈ HL → ∃!𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)))
22 glbcon.o . . . . 5 = (oc‘𝐾)
23 breq1 4891 . . . . . . 7 (𝑦 = ( 𝑣) → (𝑦(le‘𝐾)𝑧 ↔ ( 𝑣)(le‘𝐾)𝑧))
2423ralbidv 3168 . . . . . 6 (𝑦 = ( 𝑣) → (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧))
25 breq2 4892 . . . . . . . 8 (𝑦 = ( 𝑣) → (𝑤(le‘𝐾)𝑦𝑤(le‘𝐾)( 𝑣)))
2625imbi2d 332 . . . . . . 7 (𝑦 = ( 𝑣) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))
2726ralbidv 3168 . . . . . 6 (𝑦 = ( 𝑣) → (∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦) ↔ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))
2824, 27anbi12d 624 . . . . 5 (𝑦 = ( 𝑣) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)))))
296, 22, 28riotaocN 35372 . . . 4 ((𝐾 ∈ OP ∧ ∃!𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) → (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) = ( ‘(𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))))
3014, 21, 29syl2anc 579 . . 3 (𝐾 ∈ HL → (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) = ( ‘(𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))))
3114ad2antrr 716 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → 𝐾 ∈ OP)
326, 22opoccl 35357 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑢𝐵) → ( 𝑢) ∈ 𝐵)
3331, 32sylancom 582 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → ( 𝑢) ∈ 𝐵)
3414ad2antrr 716 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → 𝐾 ∈ OP)
356, 22opoccl 35357 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑧𝐵) → ( 𝑧) ∈ 𝐵)
3634, 35sylancom 582 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → ( 𝑧) ∈ 𝐵)
376, 22opococ 35358 . . . . . . . . . . . . 13 ((𝐾 ∈ OP ∧ 𝑧𝐵) → ( ‘( 𝑧)) = 𝑧)
3834, 37sylancom 582 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → ( ‘( 𝑧)) = 𝑧)
3938eqcomd 2784 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → 𝑧 = ( ‘( 𝑧)))
40 fveq2 6448 . . . . . . . . . . . 12 (𝑢 = ( 𝑧) → ( 𝑢) = ( ‘( 𝑧)))
4140rspceeqv 3529 . . . . . . . . . . 11 ((( 𝑧) ∈ 𝐵𝑧 = ( ‘( 𝑧))) → ∃𝑢𝐵 𝑧 = ( 𝑢))
4236, 39, 41syl2anc 579 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → ∃𝑢𝐵 𝑧 = ( 𝑢))
43 eleq1 2847 . . . . . . . . . . . 12 (𝑧 = ( 𝑢) → (𝑧𝑆 ↔ ( 𝑢) ∈ 𝑆))
44 breq2 4892 . . . . . . . . . . . 12 (𝑧 = ( 𝑢) → (( 𝑣)(le‘𝐾)𝑧 ↔ ( 𝑣)(le‘𝐾)( 𝑢)))
4543, 44imbi12d 336 . . . . . . . . . . 11 (𝑧 = ( 𝑢) → ((𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
4645adantl 475 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧 = ( 𝑢)) → ((𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
4733, 42, 46ralxfrd 5122 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑧𝐵 (𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
48 simpr 479 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → 𝑢𝐵)
49 simplr 759 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → 𝑣𝐵)
506, 7, 22oplecon3b 35363 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑢𝐵𝑣𝐵) → (𝑢(le‘𝐾)𝑣 ↔ ( 𝑣)(le‘𝐾)( 𝑢)))
5131, 48, 49, 50syl3anc 1439 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → (𝑢(le‘𝐾)𝑣 ↔ ( 𝑣)(le‘𝐾)( 𝑢)))
5251imbi2d 332 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → ((( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
5352ralbidva 3167 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
5447, 53bitr4d 274 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑧𝐵 (𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣)))
55 eleq1 2847 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥𝑆𝑧𝑆))
5655ralrab 3578 . . . . . . . 8 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ↔ ∀𝑧𝐵 (𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧))
57 fveq2 6448 . . . . . . . . . 10 (𝑥 = 𝑢 → ( 𝑥) = ( 𝑢))
5857eleq1d 2844 . . . . . . . . 9 (𝑥 = 𝑢 → (( 𝑥) ∈ 𝑆 ↔ ( 𝑢) ∈ 𝑆))
5958ralrab 3578 . . . . . . . 8 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣))
6054, 56, 593bitr4g 306 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ↔ ∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣))
6114ad2antrr 716 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → 𝐾 ∈ OP)
626, 22opoccl 35357 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑡𝐵) → ( 𝑡) ∈ 𝐵)
6361, 62sylancom 582 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → ( 𝑡) ∈ 𝐵)
6414ad2antrr 716 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → 𝐾 ∈ OP)
656, 22opoccl 35357 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑤𝐵) → ( 𝑤) ∈ 𝐵)
6664, 65sylancom 582 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → ( 𝑤) ∈ 𝐵)
676, 22opococ 35358 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑤𝐵) → ( ‘( 𝑤)) = 𝑤)
6864, 67sylancom 582 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → ( ‘( 𝑤)) = 𝑤)
6968eqcomd 2784 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → 𝑤 = ( ‘( 𝑤)))
70 fveq2 6448 . . . . . . . . . . 11 (𝑡 = ( 𝑤) → ( 𝑡) = ( ‘( 𝑤)))
7170rspceeqv 3529 . . . . . . . . . 10 ((( 𝑤) ∈ 𝐵𝑤 = ( ‘( 𝑤))) → ∃𝑡𝐵 𝑤 = ( 𝑡))
7266, 69, 71syl2anc 579 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → ∃𝑡𝐵 𝑤 = ( 𝑡))
73 breq1 4891 . . . . . . . . . . . 12 (𝑤 = ( 𝑡) → (𝑤(le‘𝐾)𝑧 ↔ ( 𝑡)(le‘𝐾)𝑧))
7473ralbidv 3168 . . . . . . . . . . 11 (𝑤 = ( 𝑡) → (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧))
75 breq1 4891 . . . . . . . . . . 11 (𝑤 = ( 𝑡) → (𝑤(le‘𝐾)( 𝑣) ↔ ( 𝑡)(le‘𝐾)( 𝑣)))
7674, 75imbi12d 336 . . . . . . . . . 10 (𝑤 = ( 𝑡) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
7776adantl 475 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤 = ( 𝑡)) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
7863, 72, 77ralxfrd 5122 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ ∀𝑡𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
7914ad3antrrr 720 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → 𝐾 ∈ OP)
80 simpr 479 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → 𝑢𝐵)
81 simplr 759 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → 𝑡𝐵)
826, 7, 22oplecon3b 35363 . . . . . . . . . . . . . . 15 ((𝐾 ∈ OP ∧ 𝑢𝐵𝑡𝐵) → (𝑢(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑢)))
8379, 80, 81, 82syl3anc 1439 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → (𝑢(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑢)))
8483imbi2d 332 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → ((( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
8584ralbidva 3167 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
8679, 32sylancom 582 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → ( 𝑢) ∈ 𝐵)
8714ad3antrrr 720 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → 𝐾 ∈ OP)
8887, 35sylancom 582 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → ( 𝑧) ∈ 𝐵)
8987, 37sylancom 582 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → ( ‘( 𝑧)) = 𝑧)
9089eqcomd 2784 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → 𝑧 = ( ‘( 𝑧)))
9188, 90, 41syl2anc 579 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → ∃𝑢𝐵 𝑧 = ( 𝑢))
92 breq2 4892 . . . . . . . . . . . . . . 15 (𝑧 = ( 𝑢) → (( 𝑡)(le‘𝐾)𝑧 ↔ ( 𝑡)(le‘𝐾)( 𝑢)))
9343, 92imbi12d 336 . . . . . . . . . . . . . 14 (𝑧 = ( 𝑢) → ((𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
9493adantl 475 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧 = ( 𝑢)) → ((𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
9586, 91, 94ralxfrd 5122 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑧𝐵 (𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
9685, 95bitr4d 274 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡) ↔ ∀𝑧𝐵 (𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧)))
9758ralrab 3578 . . . . . . . . . . 11 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡))
9855ralrab 3578 . . . . . . . . . . 11 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 ↔ ∀𝑧𝐵 (𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧))
9996, 97, 983bitr4g 306 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 ↔ ∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧))
100 simplr 759 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → 𝑣𝐵)
101 simpr 479 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → 𝑡𝐵)
1026, 7, 22oplecon3b 35363 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑣𝐵𝑡𝐵) → (𝑣(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑣)))
10361, 100, 101, 102syl3anc 1439 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (𝑣(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑣)))
10499, 103imbi12d 336 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → ((∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
105104ralbidva 3167 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡) ↔ ∀𝑡𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
10678, 105bitr4d 274 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡)))
10760, 106anbi12d 624 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑣𝐵) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))) ↔ (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
108107riotabidva 6901 . . . . 5 (𝐾 ∈ HL → (𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)))) = (𝑣𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
109 ssrab2 3908 . . . . . 6 {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵
110 glbcon.u . . . . . . 7 𝑈 = (lub‘𝐾)
111 biid 253 . . . . . . 7 ((∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡)) ↔ (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡)))
112 simpl 476 . . . . . . 7 ((𝐾 ∈ HL ∧ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵) → 𝐾 ∈ HL)
113 simpr 479 . . . . . . 7 ((𝐾 ∈ HL ∧ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵) → {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵)
1146, 7, 110, 111, 112, 113lubval 17381 . . . . . 6 ((𝐾 ∈ HL ∧ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵) → (𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}) = (𝑣𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
115109, 114mpan2 681 . . . . 5 (𝐾 ∈ HL → (𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}) = (𝑣𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
116108, 115eqtr4d 2817 . . . 4 (𝐾 ∈ HL → (𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)))) = (𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}))
117116fveq2d 6452 . . 3 (𝐾 ∈ HL → ( ‘(𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))) = ( ‘(𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆})))
11813, 30, 1173eqtrd 2818 . 2 (𝐾 ∈ HL → (𝐺‘{𝑥𝐵𝑥𝑆}) = ( ‘(𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆})))
1195, 118sylan9eqr 2836 1 ((𝐾 ∈ HL ∧ 𝑆𝐵) → (𝐺𝑆) = ( ‘(𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wcel 2107  wral 3090  wrex 3091  ∃!wreu 3092  {crab 3094  cin 3791  wss 3792   class class class wbr 4888  cfv 6137  crio 6884  Basecbs 16266  lecple 16356  occoc 16357  lubclub 17339  glbcglb 17340  CLatccla 17504  OPcops 35335  HLchlt 35513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5008  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-riotaBAD 35116
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-iun 4757  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-riota 6885  df-ov 6927  df-undef 7683  df-lub 17371  df-glb 17372  df-clat 17505  df-oposet 35339  df-ol 35341  df-oml 35342  df-hlat 35514
This theorem is referenced by:  glbconxN  35541
  Copyright terms: Public domain W3C validator