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 35336
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 3742 . . . 4 (𝐵𝑆) = {𝑥𝐵𝑥𝑆}
2 sseqin2 3981 . . . . 5 (𝑆𝐵 ↔ (𝐵𝑆) = 𝑆)
32biimpi 207 . . . 4 (𝑆𝐵 → (𝐵𝑆) = 𝑆)
41, 3syl5reqr 2814 . . 3 (𝑆𝐵𝑆 = {𝑥𝐵𝑥𝑆})
54fveq2d 6381 . 2 (𝑆𝐵 → (𝐺𝑆) = (𝐺‘{𝑥𝐵𝑥𝑆}))
6 glbcon.b . . . 4 𝐵 = (Base‘𝐾)
7 eqid 2765 . . . 4 (le‘𝐾) = (le‘𝐾)
8 glbcon.g . . . 4 𝐺 = (glb‘𝐾)
9 biid 252 . . . 4 ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)))
10 id 22 . . . 4 (𝐾 ∈ HL → 𝐾 ∈ HL)
11 ssrab2 3849 . . . . 5 {𝑥𝐵𝑥𝑆} ⊆ 𝐵
1211a1i 11 . . . 4 (𝐾 ∈ HL → {𝑥𝐵𝑥𝑆} ⊆ 𝐵)
136, 7, 8, 9, 10, 12glbval 17266 . . 3 (𝐾 ∈ HL → (𝐺‘{𝑥𝐵𝑥𝑆}) = (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))))
14 hlop 35321 . . . 4 (𝐾 ∈ HL → 𝐾 ∈ OP)
15 hlclat 35317 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ CLat)
166, 8clatglbcl 17383 . . . . . . 7 ((𝐾 ∈ CLat ∧ {𝑥𝐵𝑥𝑆} ⊆ 𝐵) → (𝐺‘{𝑥𝐵𝑥𝑆}) ∈ 𝐵)
1715, 11, 16sylancl 580 . . . . . 6 (𝐾 ∈ HL → (𝐺‘{𝑥𝐵𝑥𝑆}) ∈ 𝐵)
1813, 17eqeltrrd 2845 . . . . 5 (𝐾 ∈ HL → (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) ∈ 𝐵)
196fvexi 6391 . . . . . 6 𝐵 ∈ V
2019riotaclbBAD 34914 . . . . 5 (∃!𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)) ↔ (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) ∈ 𝐵)
2118, 20sylibr 225 . . . 4 (𝐾 ∈ HL → ∃!𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)))
22 glbcon.o . . . . 5 = (oc‘𝐾)
23 breq1 4814 . . . . . . 7 (𝑦 = ( 𝑣) → (𝑦(le‘𝐾)𝑧 ↔ ( 𝑣)(le‘𝐾)𝑧))
2423ralbidv 3133 . . . . . 6 (𝑦 = ( 𝑣) → (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧))
25 breq2 4815 . . . . . . . 8 (𝑦 = ( 𝑣) → (𝑤(le‘𝐾)𝑦𝑤(le‘𝐾)( 𝑣)))
2625imbi2d 331 . . . . . . 7 (𝑦 = ( 𝑣) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))
2726ralbidv 3133 . . . . . 6 (𝑦 = ( 𝑣) → (∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦) ↔ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))
2824, 27anbi12d 624 . . . . 5 (𝑦 = ( 𝑣) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)))))
296, 22, 28riotaocN 35168 . . . 4 ((𝐾 ∈ OP ∧ ∃!𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) → (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) = ( ‘(𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))))
3014, 21, 29syl2anc 579 . . 3 (𝐾 ∈ HL → (𝑦𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)𝑦))) = ( ‘(𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))))
3114ad2antrr 717 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → 𝐾 ∈ OP)
326, 22opoccl 35153 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑢𝐵) → ( 𝑢) ∈ 𝐵)
3331, 32sylancom 582 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → ( 𝑢) ∈ 𝐵)
3414ad2antrr 717 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → 𝐾 ∈ OP)
356, 22opoccl 35153 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑧𝐵) → ( 𝑧) ∈ 𝐵)
3634, 35sylancom 582 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → ( 𝑧) ∈ 𝐵)
376, 22opococ 35154 . . . . . . . . . . . . 13 ((𝐾 ∈ OP ∧ 𝑧𝐵) → ( ‘( 𝑧)) = 𝑧)
3834, 37sylancom 582 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → ( ‘( 𝑧)) = 𝑧)
3938eqcomd 2771 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → 𝑧 = ( ‘( 𝑧)))
40 fveq2 6377 . . . . . . . . . . . 12 (𝑢 = ( 𝑧) → ( 𝑢) = ( ‘( 𝑧)))
4140rspceeqv 3480 . . . . . . . . . . 11 ((( 𝑧) ∈ 𝐵𝑧 = ( ‘( 𝑧))) → ∃𝑢𝐵 𝑧 = ( 𝑢))
4236, 39, 41syl2anc 579 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧𝐵) → ∃𝑢𝐵 𝑧 = ( 𝑢))
43 eleq1 2832 . . . . . . . . . . . 12 (𝑧 = ( 𝑢) → (𝑧𝑆 ↔ ( 𝑢) ∈ 𝑆))
44 breq2 4815 . . . . . . . . . . . 12 (𝑧 = ( 𝑢) → (( 𝑣)(le‘𝐾)𝑧 ↔ ( 𝑣)(le‘𝐾)( 𝑢)))
4543, 44imbi12d 335 . . . . . . . . . . 11 (𝑧 = ( 𝑢) → ((𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
4645adantl 473 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑧 = ( 𝑢)) → ((𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
4733, 42, 46ralxfrd 5045 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑧𝐵 (𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
48 simpr 477 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → 𝑢𝐵)
49 simplr 785 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → 𝑣𝐵)
506, 7, 22oplecon3b 35159 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑢𝐵𝑣𝐵) → (𝑢(le‘𝐾)𝑣 ↔ ( 𝑣)(le‘𝐾)( 𝑢)))
5131, 48, 49, 50syl3anc 1490 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → (𝑢(le‘𝐾)𝑣 ↔ ( 𝑣)(le‘𝐾)( 𝑢)))
5251imbi2d 331 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑢𝐵) → ((( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
5352ralbidva 3132 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑣)(le‘𝐾)( 𝑢))))
5447, 53bitr4d 273 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑧𝐵 (𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣)))
55 eleq1 2832 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥𝑆𝑧𝑆))
5655ralrab 3527 . . . . . . . 8 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ↔ ∀𝑧𝐵 (𝑧𝑆 → ( 𝑣)(le‘𝐾)𝑧))
57 fveq2 6377 . . . . . . . . . 10 (𝑥 = 𝑢 → ( 𝑥) = ( 𝑢))
5857eleq1d 2829 . . . . . . . . 9 (𝑥 = 𝑢 → (( 𝑥) ∈ 𝑆 ↔ ( 𝑢) ∈ 𝑆))
5958ralrab 3527 . . . . . . . 8 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑣))
6054, 56, 593bitr4g 305 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ↔ ∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣))
6114ad2antrr 717 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → 𝐾 ∈ OP)
626, 22opoccl 35153 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑡𝐵) → ( 𝑡) ∈ 𝐵)
6361, 62sylancom 582 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → ( 𝑡) ∈ 𝐵)
6414ad2antrr 717 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → 𝐾 ∈ OP)
656, 22opoccl 35153 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑤𝐵) → ( 𝑤) ∈ 𝐵)
6664, 65sylancom 582 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → ( 𝑤) ∈ 𝐵)
676, 22opococ 35154 . . . . . . . . . . . 12 ((𝐾 ∈ OP ∧ 𝑤𝐵) → ( ‘( 𝑤)) = 𝑤)
6864, 67sylancom 582 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → ( ‘( 𝑤)) = 𝑤)
6968eqcomd 2771 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → 𝑤 = ( ‘( 𝑤)))
70 fveq2 6377 . . . . . . . . . . 11 (𝑡 = ( 𝑤) → ( 𝑡) = ( ‘( 𝑤)))
7170rspceeqv 3480 . . . . . . . . . 10 ((( 𝑤) ∈ 𝐵𝑤 = ( ‘( 𝑤))) → ∃𝑡𝐵 𝑤 = ( 𝑡))
7266, 69, 71syl2anc 579 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤𝐵) → ∃𝑡𝐵 𝑤 = ( 𝑡))
73 breq1 4814 . . . . . . . . . . . 12 (𝑤 = ( 𝑡) → (𝑤(le‘𝐾)𝑧 ↔ ( 𝑡)(le‘𝐾)𝑧))
7473ralbidv 3133 . . . . . . . . . . 11 (𝑤 = ( 𝑡) → (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧))
75 breq1 4814 . . . . . . . . . . 11 (𝑤 = ( 𝑡) → (𝑤(le‘𝐾)( 𝑣) ↔ ( 𝑡)(le‘𝐾)( 𝑣)))
7674, 75imbi12d 335 . . . . . . . . . 10 (𝑤 = ( 𝑡) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
7776adantl 473 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑤 = ( 𝑡)) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
7863, 72, 77ralxfrd 5045 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ ∀𝑡𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
7914ad3antrrr 721 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → 𝐾 ∈ OP)
80 simpr 477 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → 𝑢𝐵)
81 simplr 785 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → 𝑡𝐵)
826, 7, 22oplecon3b 35159 . . . . . . . . . . . . . . 15 ((𝐾 ∈ OP ∧ 𝑢𝐵𝑡𝐵) → (𝑢(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑢)))
8379, 80, 81, 82syl3anc 1490 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → (𝑢(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑢)))
8483imbi2d 331 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → ((( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
8584ralbidva 3132 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
8679, 32sylancom 582 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑢𝐵) → ( 𝑢) ∈ 𝐵)
8714ad3antrrr 721 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → 𝐾 ∈ OP)
8887, 35sylancom 582 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → ( 𝑧) ∈ 𝐵)
8987, 37sylancom 582 . . . . . . . . . . . . . . 15 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → ( ‘( 𝑧)) = 𝑧)
9089eqcomd 2771 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → 𝑧 = ( ‘( 𝑧)))
9188, 90, 41syl2anc 579 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧𝐵) → ∃𝑢𝐵 𝑧 = ( 𝑢))
92 breq2 4815 . . . . . . . . . . . . . . 15 (𝑧 = ( 𝑢) → (( 𝑡)(le‘𝐾)𝑧 ↔ ( 𝑡)(le‘𝐾)( 𝑢)))
9343, 92imbi12d 335 . . . . . . . . . . . . . 14 (𝑧 = ( 𝑢) → ((𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
9493adantl 473 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) ∧ 𝑧 = ( 𝑢)) → ((𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧) ↔ (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
9586, 91, 94ralxfrd 5045 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑧𝐵 (𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧) ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆 → ( 𝑡)(le‘𝐾)( 𝑢))))
9685, 95bitr4d 273 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡) ↔ ∀𝑧𝐵 (𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧)))
9758ralrab 3527 . . . . . . . . . . 11 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 ↔ ∀𝑢𝐵 (( 𝑢) ∈ 𝑆𝑢(le‘𝐾)𝑡))
9855ralrab 3527 . . . . . . . . . . 11 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 ↔ ∀𝑧𝐵 (𝑧𝑆 → ( 𝑡)(le‘𝐾)𝑧))
9996, 97, 983bitr4g 305 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 ↔ ∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧))
100 simplr 785 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → 𝑣𝐵)
101 simpr 477 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → 𝑡𝐵)
1026, 7, 22oplecon3b 35159 . . . . . . . . . . 11 ((𝐾 ∈ OP ∧ 𝑣𝐵𝑡𝐵) → (𝑣(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑣)))
10361, 100, 101, 102syl3anc 1490 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → (𝑣(le‘𝐾)𝑡 ↔ ( 𝑡)(le‘𝐾)( 𝑣)))
10499, 103imbi12d 335 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑣𝐵) ∧ 𝑡𝐵) → ((∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡) ↔ (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
105104ralbidva 3132 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡) ↔ ∀𝑡𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑡)(le‘𝐾)𝑧 → ( 𝑡)(le‘𝐾)( 𝑣))))
10678, 105bitr4d 273 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑣𝐵) → (∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)) ↔ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡)))
10760, 106anbi12d 624 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑣𝐵) → ((∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))) ↔ (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
108107riotabidva 6821 . . . . 5 (𝐾 ∈ HL → (𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)))) = (𝑣𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
109 ssrab2 3849 . . . . . 6 {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵
110 glbcon.u . . . . . . 7 𝑈 = (lub‘𝐾)
111 biid 252 . . . . . . 7 ((∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡)) ↔ (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡)))
112 simpl 474 . . . . . . 7 ((𝐾 ∈ HL ∧ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵) → 𝐾 ∈ HL)
113 simpr 477 . . . . . . 7 ((𝐾 ∈ HL ∧ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵) → {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵)
1146, 7, 110, 111, 112, 113lubval 17253 . . . . . 6 ((𝐾 ∈ HL ∧ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆} ⊆ 𝐵) → (𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}) = (𝑣𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
115109, 114mpan2 682 . . . . 5 (𝐾 ∈ HL → (𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}) = (𝑣𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡𝐵 (∀𝑢 ∈ {𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡𝑣(le‘𝐾)𝑡))))
116108, 115eqtr4d 2802 . . . 4 (𝐾 ∈ HL → (𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣)))) = (𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆}))
117116fveq2d 6381 . . 3 (𝐾 ∈ HL → ( ‘(𝑣𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆} ( 𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤𝐵 (∀𝑧 ∈ {𝑥𝐵𝑥𝑆}𝑤(le‘𝐾)𝑧𝑤(le‘𝐾)( 𝑣))))) = ( ‘(𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆})))
11813, 30, 1173eqtrd 2803 . 2 (𝐾 ∈ HL → (𝐺‘{𝑥𝐵𝑥𝑆}) = ( ‘(𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆})))
1195, 118sylan9eqr 2821 1 ((𝐾 ∈ HL ∧ 𝑆𝐵) → (𝐺𝑆) = ( ‘(𝑈‘{𝑥𝐵 ∣ ( 𝑥) ∈ 𝑆})))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  wrex 3056  ∃!wreu 3057  {crab 3059  cin 3733  wss 3734   class class class wbr 4811  cfv 6070  crio 6804  Basecbs 16133  lecple 16224  occoc 16225  lubclub 17211  glbcglb 17212  CLatccla 17376  OPcops 35131  HLchlt 35309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-riotaBAD 34912
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-id 5187  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6805  df-ov 6847  df-undef 7604  df-lub 17243  df-glb 17244  df-clat 17377  df-oposet 35135  df-ol 35137  df-oml 35138  df-hlat 35310
This theorem is referenced by:  glbconxN  35337
  Copyright terms: Public domain W3C validator