Theorem glbconN 37391

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.

Step	Hyp	Ref	Expression
1		sseqin2 4149	. . . . 5 ⊢ (𝑆 ⊆ 𝐵 ↔ (𝐵 ∩ 𝑆) = 𝑆)
2	1	biimpi 215	. . . 4 ⊢ (𝑆 ⊆ 𝐵 → (𝐵 ∩ 𝑆) = 𝑆)
3		dfin5 3895	. . . 4 ⊢ (𝐵 ∩ 𝑆) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}
4	2, 3	eqtr3di 2793	. . 3 ⊢ (𝑆 ⊆ 𝐵 → 𝑆 = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆})
5	4	fveq2d 6778	. 2 ⊢ (𝑆 ⊆ 𝐵 → (𝐺‘𝑆) = (𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}))
6		glbcon.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
7		eqid 2738	. . . 4 ⊢ (le‘𝐾) = (le‘𝐾)
8		glbcon.g	. . . 4 ⊢ 𝐺 = (glb‘𝐾)
9		biid 260	. . . 4 ⊢ ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦)) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦)))
10		id 22	. . . 4 ⊢ (𝐾 ∈ HL → 𝐾 ∈ HL)
11		ssrab2 4013	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ⊆ 𝐵
12	11	a1i 11	. . . 4 ⊢ (𝐾 ∈ HL → {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ⊆ 𝐵)
13	6, 7, 8, 9, 10, 12	glbval 18087	. . 3 ⊢ (𝐾 ∈ HL → (𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}) = (℩𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦))))
14		hlop 37376	. . . 4 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
15		hlclat 37372	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
16	6, 8	clatglbcl 18223	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ⊆ 𝐵) → (𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}) ∈ 𝐵)
17	15, 11, 16	sylancl 586	. . . . . 6 ⊢ (𝐾 ∈ HL → (𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}) ∈ 𝐵)
18	13, 17	eqeltrrd 2840	. . . . 5 ⊢ (𝐾 ∈ HL → (℩𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦))) ∈ 𝐵)
19	6	fvexi 6788	. . . . . 6 ⊢ 𝐵 ∈ V
20	19	riotaclbBAD 36969	. . . . 5 ⊢ (∃!𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦)) ↔ (℩𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦))) ∈ 𝐵)
21	18, 20	sylibr 233	. . . 4 ⊢ (𝐾 ∈ HL → ∃!𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦)))
22		glbcon.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
23		breq1 5077	. . . . . . 7 ⊢ (𝑦 = ( ⊥ ‘𝑣) → (𝑦(le‘𝐾)𝑧 ↔ ( ⊥ ‘𝑣)(le‘𝐾)𝑧))
24	23	ralbidv 3112	. . . . . 6 ⊢ (𝑦 = ( ⊥ ‘𝑣) → (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧))
25		breq2 5078	. . . . . . . 8 ⊢ (𝑦 = ( ⊥ ‘𝑣) → (𝑤(le‘𝐾)𝑦 ↔ 𝑤(le‘𝐾)( ⊥ ‘𝑣)))
26	25	imbi2d 341	. . . . . . 7 ⊢ (𝑦 = ( ⊥ ‘𝑣) → ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣))))
27	26	ralbidv 3112	. . . . . 6 ⊢ (𝑦 = ( ⊥ ‘𝑣) → (∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦) ↔ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣))))
28	24, 27	anbi12d 631	. . . . 5 ⊢ (𝑦 = ( ⊥ ‘𝑣) → ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦)) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)))))
29	6, 22, 28	riotaocN 37223	. . . 4 ⊢ ((𝐾 ∈ OP ∧ ∃!𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦))) → (℩𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦))) = ( ⊥ ‘(℩𝑣 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣))))))
30	14, 21, 29	syl2anc 584	. . 3 ⊢ (𝐾 ∈ HL → (℩𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦))) = ( ⊥ ‘(℩𝑣 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣))))))
31	14	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝐾 ∈ OP)
32	6, 22	opoccl 37208	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵) → ( ⊥ ‘𝑢) ∈ 𝐵)
33	31, 32	sylancom 588	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ( ⊥ ‘𝑢) ∈ 𝐵)
34	14	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝐾 ∈ OP)
35	6, 22	opoccl 37208	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OP ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘𝑧) ∈ 𝐵)
36	34, 35	sylancom 588	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘𝑧) ∈ 𝐵)
37	6, 22	opococ 37209	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OP ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑧)) = 𝑧)
38	34, 37	sylancom 588	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑧)) = 𝑧)
39	38	eqcomd 2744	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 = ( ⊥ ‘( ⊥ ‘𝑧)))
40		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑢 = ( ⊥ ‘𝑧) → ( ⊥ ‘𝑢) = ( ⊥ ‘( ⊥ ‘𝑧)))
41	40	rspceeqv 3575	. . . . . . . . . . 11 ⊢ ((( ⊥ ‘𝑧) ∈ 𝐵 ∧ 𝑧 = ( ⊥ ‘( ⊥ ‘𝑧))) → ∃𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘𝑢))
42	36, 39, 41	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ∃𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘𝑢))
43		eleq1 2826	. . . . . . . . . . . 12 ⊢ (𝑧 = ( ⊥ ‘𝑢) → (𝑧 ∈ 𝑆 ↔ ( ⊥ ‘𝑢) ∈ 𝑆))
44		breq2 5078	. . . . . . . . . . . 12 ⊢ (𝑧 = ( ⊥ ‘𝑢) → (( ⊥ ‘𝑣)(le‘𝐾)𝑧 ↔ ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢)))
45	43, 44	imbi12d 345	. . . . . . . . . . 11 ⊢ (𝑧 = ( ⊥ ‘𝑢) → ((𝑧 ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)𝑧) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢))))
46	45	adantl 482	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 = ( ⊥ ‘𝑢)) → ((𝑧 ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)𝑧) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢))))
47	33, 42, 46	ralxfrd 5331	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)𝑧) ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢))))
48		simpr 485	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ 𝐵)
49		simplr 766	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝑣 ∈ 𝐵)
50	6, 7, 22	oplecon3b 37214	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(le‘𝐾)𝑣 ↔ ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢)))
51	31, 48, 49, 50	syl3anc 1370	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → (𝑢(le‘𝐾)𝑣 ↔ ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢)))
52	51	imbi2d 341	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ((( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑣) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢))))
53	52	ralbidva 3111	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑣) ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢))))
54	47, 53	bitr4d 281	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)𝑧) ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑣)))
55		eleq1 2826	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑆 ↔ 𝑧 ∈ 𝑆))
56	55	ralrab 3630	. . . . . . . 8 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)𝑧))
57		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑢))
58	57	eleq1d 2823	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (( ⊥ ‘𝑥) ∈ 𝑆 ↔ ( ⊥ ‘𝑢) ∈ 𝑆))
59	58	ralrab 3630	. . . . . . . 8 ⊢ (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑣))
60	54, 56, 59	3bitr4g 314	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ↔ ∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣))
61	14	ad2antrr 723	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → 𝐾 ∈ OP)
62	6, 22	opoccl 37208	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑡 ∈ 𝐵) → ( ⊥ ‘𝑡) ∈ 𝐵)
63	61, 62	sylancom 588	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → ( ⊥ ‘𝑡) ∈ 𝐵)
64	14	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) → 𝐾 ∈ OP)
65	6, 22	opoccl 37208	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ 𝑤 ∈ 𝐵) → ( ⊥ ‘𝑤) ∈ 𝐵)
66	64, 65	sylancom 588	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) → ( ⊥ ‘𝑤) ∈ 𝐵)
67	6, 22	opococ 37209	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OP ∧ 𝑤 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑤)) = 𝑤)
68	64, 67	sylancom 588	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑤)) = 𝑤)
69	68	eqcomd 2744	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) → 𝑤 = ( ⊥ ‘( ⊥ ‘𝑤)))
70		fveq2 6774	. . . . . . . . . . 11 ⊢ (𝑡 = ( ⊥ ‘𝑤) → ( ⊥ ‘𝑡) = ( ⊥ ‘( ⊥ ‘𝑤)))
71	70	rspceeqv 3575	. . . . . . . . . 10 ⊢ ((( ⊥ ‘𝑤) ∈ 𝐵 ∧ 𝑤 = ( ⊥ ‘( ⊥ ‘𝑤))) → ∃𝑡 ∈ 𝐵 𝑤 = ( ⊥ ‘𝑡))
72	66, 69, 71	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) → ∃𝑡 ∈ 𝐵 𝑤 = ( ⊥ ‘𝑡))
73		breq1 5077	. . . . . . . . . . . 12 ⊢ (𝑤 = ( ⊥ ‘𝑡) → (𝑤(le‘𝐾)𝑧 ↔ ( ⊥ ‘𝑡)(le‘𝐾)𝑧))
74	73	ralbidv 3112	. . . . . . . . . . 11 ⊢ (𝑤 = ( ⊥ ‘𝑡) → (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧))
75		breq1 5077	. . . . . . . . . . 11 ⊢ (𝑤 = ( ⊥ ‘𝑡) → (𝑤(le‘𝐾)( ⊥ ‘𝑣) ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣)))
76	74, 75	imbi12d 345	. . . . . . . . . 10 ⊢ (𝑤 = ( ⊥ ‘𝑡) → ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣))))
77	76	adantl 482	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 = ( ⊥ ‘𝑡)) → ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣))))
78	63, 72, 77	ralxfrd 5331	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)) ↔ ∀𝑡 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣))))
79	14	ad3antrrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝐾 ∈ OP)
80		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ 𝐵)
81		simplr 766	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝑡 ∈ 𝐵)
82	6, 7, 22	oplecon3b 37214	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → (𝑢(le‘𝐾)𝑡 ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢)))
83	79, 80, 81, 82	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → (𝑢(le‘𝐾)𝑡 ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢)))
84	83	imbi2d 341	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ((( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑡) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢))))
85	84	ralbidva 3111	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑡) ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢))))
86	79, 32	sylancom 588	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ( ⊥ ‘𝑢) ∈ 𝐵)
87	14	ad3antrrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝐾 ∈ OP)
88	87, 35	sylancom 588	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘𝑧) ∈ 𝐵)
89	87, 37	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑧)) = 𝑧)
90	89	eqcomd 2744	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 = ( ⊥ ‘( ⊥ ‘𝑧)))
91	88, 90, 41	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ∃𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘𝑢))
92		breq2 5078	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ( ⊥ ‘𝑢) → (( ⊥ ‘𝑡)(le‘𝐾)𝑧 ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢)))
93	43, 92	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ( ⊥ ‘𝑢) → ((𝑧 ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)𝑧) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢))))
94	93	adantl 482	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 = ( ⊥ ‘𝑢)) → ((𝑧 ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)𝑧) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢))))
95	86, 91, 94	ralxfrd 5331	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)𝑧) ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢))))
96	85, 95	bitr4d 281	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑡) ↔ ∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)𝑧)))
97	58	ralrab 3630	. . . . . . . . . . 11 ⊢ (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑡))
98	55	ralrab 3630	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)𝑧))
99	96, 97, 98	3bitr4g 314	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧))
100		simplr 766	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → 𝑣 ∈ 𝐵)
101		simpr 485	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ 𝐵)
102	6, 7, 22	oplecon3b 37214	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ 𝑣 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → (𝑣(le‘𝐾)𝑡 ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣)))
103	61, 100, 101, 102	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (𝑣(le‘𝐾)𝑡 ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣)))
104	99, 103	imbi12d 345	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → ((∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣))))
105	104	ralbidva 3111	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡) ↔ ∀𝑡 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣))))
106	78, 105	bitr4d 281	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)) ↔ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡)))
107	60, 106	anbi12d 631	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣))) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡))))
108	107	riotabidva 7252	. . . . 5 ⊢ (𝐾 ∈ HL → (℩𝑣 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)))) = (℩𝑣 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡))))
109		ssrab2 4013	. . . . . 6 ⊢ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆} ⊆ 𝐵
110		glbcon.u	. . . . . . 7 ⊢ 𝑈 = (lub‘𝐾)
111		biid 260	. . . . . . 7 ⊢ ((∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡)) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡)))
112		simpl 483	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆} ⊆ 𝐵) → 𝐾 ∈ HL)
113		simpr 485	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆} ⊆ 𝐵) → {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆} ⊆ 𝐵)
114	6, 7, 110, 111, 112, 113	lubval 18074	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆} ⊆ 𝐵) → (𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}) = (℩𝑣 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡))))
115	109, 114	mpan2 688	. . . . 5 ⊢ (𝐾 ∈ HL → (𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}) = (℩𝑣 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡))))
116	108, 115	eqtr4d 2781	. . . 4 ⊢ (𝐾 ∈ HL → (℩𝑣 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)))) = (𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}))
117	116	fveq2d 6778	. . 3 ⊢ (𝐾 ∈ HL → ( ⊥ ‘(℩𝑣 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣))))) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆})))
118	13, 30, 117	3eqtrd 2782	. 2 ⊢ (𝐾 ∈ HL → (𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆})))
119	5, 118	sylan9eqr 2800	1 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆})))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ∃wrex 3065  ∃!wreu 3066  {crab 3068   ∩ cin 3886   ⊆ wss 3887   class class class wbr 5074  ‘cfv 6433  ℩crio 7231  Basecbs 16912  lecple 16969  occoc 16970  lubclub 18027  glbcglb 18028  CLatccla 18216  OPcops 37186  HLchlt 37364

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-riotaBAD 36967

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-undef 8089  df-lub 18064  df-glb 18065  df-clat 18217  df-oposet 37190  df-ol 37192  df-oml 37193  df-hlat 37365

This theorem is referenced by:  glbconxN  37392