Theorem glbconNOLD 39360

Description: Obsolete version of glbconN 39359 as of 3-Jan-2025. (Contributed by NM, 17-Jan-2012.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
glbcon.b	⊢ 𝐵 = (Base‘𝐾)
glbcon.u	⊢ 𝑈 = (lub‘𝐾)
glbcon.g	⊢ 𝐺 = (glb‘𝐾)
glbcon.o	⊢ ⊥ = (oc‘𝐾)

Assertion

Ref	Expression
glbconNOLD	⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆})))

Distinct variable groups:   𝑥,𝐵   𝑥, ⊥   𝑥,𝑆

Allowed substitution hints:   𝑈(𝑥)   𝐺(𝑥)   𝐾(𝑥)

Proof of Theorem glbconNOLD

Dummy variables 𝑢 𝑡 𝑣 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseqin2 4231	. . . . 5 ⊢ (𝑆 ⊆ 𝐵 ↔ (𝐵 ∩ 𝑆) = 𝑆)
2	1	biimpi 216	. . . 4 ⊢ (𝑆 ⊆ 𝐵 → (𝐵 ∩ 𝑆) = 𝑆)
3		dfin5 3971	. . . 4 ⊢ (𝐵 ∩ 𝑆) = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}
4	2, 3	eqtr3di 2790	. . 3 ⊢ (𝑆 ⊆ 𝐵 → 𝑆 = {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆})
5	4	fveq2d 6911	. 2 ⊢ (𝑆 ⊆ 𝐵 → (𝐺‘𝑆) = (𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}))
6		glbcon.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
7		eqid 2735	. . . 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 4090	. . . . 5 ⊢ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ⊆ 𝐵
12	11	a1i 11	. . . 4 ⊢ (𝐾 ∈ HL → {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ⊆ 𝐵)
13	6, 7, 8, 9, 10, 12	glbval 18427	. . 3 ⊢ (𝐾 ∈ HL → (𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}) = (℩𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦))))
14		hlop 39344	. . . 4 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
15		hlclat 39340	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat)
16	6, 8	clatglbcl 18563	. . . . . . 7 ⊢ ((𝐾 ∈ CLat ∧ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ⊆ 𝐵) → (𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}) ∈ 𝐵)
17	15, 11, 16	sylancl 586	. . . . . 6 ⊢ (𝐾 ∈ HL → (𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}) ∈ 𝐵)
18	13, 17	eqeltrrd 2840	. . . . 5 ⊢ (𝐾 ∈ HL → (℩𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦))) ∈ 𝐵)
19	6	fvexi 6921	. . . . . 6 ⊢ 𝐵 ∈ V
20	19	riotaclbBAD 38937	. . . . 5 ⊢ (∃!𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦)) ↔ (℩𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦))) ∈ 𝐵)
21	18, 20	sylibr 234	. . . 4 ⊢ (𝐾 ∈ HL → ∃!𝑦 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦)))
22		glbcon.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
23		breq1 5151	. . . . . . 7 ⊢ (𝑦 = ( ⊥ ‘𝑣) → (𝑦(le‘𝐾)𝑧 ↔ ( ⊥ ‘𝑣)(le‘𝐾)𝑧))
24	23	ralbidv 3176	. . . . . 6 ⊢ (𝑦 = ( ⊥ ‘𝑣) → (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧))
25		breq2 5152	. . . . . . . 8 ⊢ (𝑦 = ( ⊥ ‘𝑣) → (𝑤(le‘𝐾)𝑦 ↔ 𝑤(le‘𝐾)( ⊥ ‘𝑣)))
26	25	imbi2d 340	. . . . . . 7 ⊢ (𝑦 = ( ⊥ ‘𝑣) → ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣))))
27	26	ralbidv 3176	. . . . . 6 ⊢ (𝑦 = ( ⊥ ‘𝑣) → (∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦) ↔ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣))))
28	24, 27	anbi12d 632	. . . . 5 ⊢ (𝑦 = ( ⊥ ‘𝑣) → ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑦(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)𝑦)) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)))))
29	6, 22, 28	riotaocN 39191	. . . 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 726	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝐾 ∈ OP)
32	6, 22	opoccl 39176	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵) → ( ⊥ ‘𝑢) ∈ 𝐵)
33	31, 32	sylancom 588	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ( ⊥ ‘𝑢) ∈ 𝐵)
34	14	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝐾 ∈ OP)
35	6, 22	opoccl 39176	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OP ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘𝑧) ∈ 𝐵)
36	34, 35	sylancom 588	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘𝑧) ∈ 𝐵)
37	6, 22	opococ 39177	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ OP ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑧)) = 𝑧)
38	34, 37	sylancom 588	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑧)) = 𝑧)
39	38	eqcomd 2741	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 = ( ⊥ ‘( ⊥ ‘𝑧)))
40		fveq2 6907	. . . . . . . . . . . 12 ⊢ (𝑢 = ( ⊥ ‘𝑧) → ( ⊥ ‘𝑢) = ( ⊥ ‘( ⊥ ‘𝑧)))
41	40	rspceeqv 3645	. . . . . . . . . . 11 ⊢ ((( ⊥ ‘𝑧) ∈ 𝐵 ∧ 𝑧 = ( ⊥ ‘( ⊥ ‘𝑧))) → ∃𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘𝑢))
42	36, 39, 41	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ∃𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘𝑢))
43		eleq1 2827	. . . . . . . . . . . 12 ⊢ (𝑧 = ( ⊥ ‘𝑢) → (𝑧 ∈ 𝑆 ↔ ( ⊥ ‘𝑢) ∈ 𝑆))
44		breq2 5152	. . . . . . . . . . . 12 ⊢ (𝑧 = ( ⊥ ‘𝑢) → (( ⊥ ‘𝑣)(le‘𝐾)𝑧 ↔ ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢)))
45	43, 44	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑧 = ( ⊥ ‘𝑢) → ((𝑧 ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)𝑧) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢))))
46	45	adantl 481	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑧 = ( ⊥ ‘𝑢)) → ((𝑧 ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)𝑧) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢))))
47	33, 42, 46	ralxfrd 5414	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)𝑧) ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢))))
48		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ 𝐵)
49		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝑣 ∈ 𝐵)
50	6, 7, 22	oplecon3b 39182	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(le‘𝐾)𝑣 ↔ ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢)))
51	31, 48, 49, 50	syl3anc 1370	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → (𝑢(le‘𝐾)𝑣 ↔ ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢)))
52	51	imbi2d 340	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ((( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑣) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢))))
53	52	ralbidva 3174	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑣) ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)( ⊥ ‘𝑢))))
54	47, 53	bitr4d 282	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)𝑧) ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑣)))
55		eleq1 2827	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑆 ↔ 𝑧 ∈ 𝑆))
56	55	ralrab 3702	. . . . . . . 8 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑣)(le‘𝐾)𝑧))
57		fveq2 6907	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑢))
58	57	eleq1d 2824	. . . . . . . . 9 ⊢ (𝑥 = 𝑢 → (( ⊥ ‘𝑥) ∈ 𝑆 ↔ ( ⊥ ‘𝑢) ∈ 𝑆))
59	58	ralrab 3702	. . . . . . . 8 ⊢ (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑣))
60	54, 56, 59	3bitr4g 314	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ↔ ∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣))
61	14	ad2antrr 726	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → 𝐾 ∈ OP)
62	6, 22	opoccl 39176	. . . . . . . . . 10 ⊢ ((𝐾 ∈ OP ∧ 𝑡 ∈ 𝐵) → ( ⊥ ‘𝑡) ∈ 𝐵)
63	61, 62	sylancom 588	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → ( ⊥ ‘𝑡) ∈ 𝐵)
64	14	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) → 𝐾 ∈ OP)
65	6, 22	opoccl 39176	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ 𝑤 ∈ 𝐵) → ( ⊥ ‘𝑤) ∈ 𝐵)
66	64, 65	sylancom 588	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) → ( ⊥ ‘𝑤) ∈ 𝐵)
67	6, 22	opococ 39177	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ OP ∧ 𝑤 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑤)) = 𝑤)
68	64, 67	sylancom 588	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑤)) = 𝑤)
69	68	eqcomd 2741	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) → 𝑤 = ( ⊥ ‘( ⊥ ‘𝑤)))
70		fveq2 6907	. . . . . . . . . . 11 ⊢ (𝑡 = ( ⊥ ‘𝑤) → ( ⊥ ‘𝑡) = ( ⊥ ‘( ⊥ ‘𝑤)))
71	70	rspceeqv 3645	. . . . . . . . . 10 ⊢ ((( ⊥ ‘𝑤) ∈ 𝐵 ∧ 𝑤 = ( ⊥ ‘( ⊥ ‘𝑤))) → ∃𝑡 ∈ 𝐵 𝑤 = ( ⊥ ‘𝑡))
72	66, 69, 71	syl2anc 584	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 ∈ 𝐵) → ∃𝑡 ∈ 𝐵 𝑤 = ( ⊥ ‘𝑡))
73		breq1 5151	. . . . . . . . . . . 12 ⊢ (𝑤 = ( ⊥ ‘𝑡) → (𝑤(le‘𝐾)𝑧 ↔ ( ⊥ ‘𝑡)(le‘𝐾)𝑧))
74	73	ralbidv 3176	. . . . . . . . . . 11 ⊢ (𝑤 = ( ⊥ ‘𝑡) → (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧))
75		breq1 5151	. . . . . . . . . . 11 ⊢ (𝑤 = ( ⊥ ‘𝑡) → (𝑤(le‘𝐾)( ⊥ ‘𝑣) ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣)))
76	74, 75	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑤 = ( ⊥ ‘𝑡) → ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣))))
77	76	adantl 481	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑤 = ( ⊥ ‘𝑡)) → ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣))))
78	63, 72, 77	ralxfrd 5414	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)) ↔ ∀𝑡 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣))))
79	14	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝐾 ∈ OP)
80		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ 𝐵)
81		simplr 769	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → 𝑡 ∈ 𝐵)
82	6, 7, 22	oplecon3b 39182	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ OP ∧ 𝑢 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → (𝑢(le‘𝐾)𝑡 ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢)))
83	79, 80, 81, 82	syl3anc 1370	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → (𝑢(le‘𝐾)𝑡 ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢)))
84	83	imbi2d 340	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ((( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑡) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢))))
85	84	ralbidva 3174	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑡) ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢))))
86	79, 32	sylancom 588	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ( ⊥ ‘𝑢) ∈ 𝐵)
87	14	ad3antrrr 730	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝐾 ∈ OP)
88	87, 35	sylancom 588	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘𝑧) ∈ 𝐵)
89	87, 37	sylancom 588	. . . . . . . . . . . . . . 15 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘𝑧)) = 𝑧)
90	89	eqcomd 2741	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → 𝑧 = ( ⊥ ‘( ⊥ ‘𝑧)))
91	88, 90, 41	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ∃𝑢 ∈ 𝐵 𝑧 = ( ⊥ ‘𝑢))
92		breq2 5152	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = ( ⊥ ‘𝑢) → (( ⊥ ‘𝑡)(le‘𝐾)𝑧 ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢)))
93	43, 92	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ( ⊥ ‘𝑢) → ((𝑧 ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)𝑧) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢))))
94	93	adantl 481	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑧 = ( ⊥ ‘𝑢)) → ((𝑧 ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)𝑧) ↔ (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢))))
95	86, 91, 94	ralxfrd 5414	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)𝑧) ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑢))))
96	85, 95	bitr4d 282	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑡) ↔ ∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)𝑧)))
97	58	ralrab 3702	. . . . . . . . . . 11 ⊢ (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 ↔ ∀𝑢 ∈ 𝐵 (( ⊥ ‘𝑢) ∈ 𝑆 → 𝑢(le‘𝐾)𝑡))
98	55	ralrab 3702	. . . . . . . . . . 11 ⊢ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 ↔ ∀𝑧 ∈ 𝐵 (𝑧 ∈ 𝑆 → ( ⊥ ‘𝑡)(le‘𝐾)𝑧))
99	96, 97, 98	3bitr4g 314	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 ↔ ∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧))
100		simplr 769	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → 𝑣 ∈ 𝐵)
101		simpr 484	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ 𝐵)
102	6, 7, 22	oplecon3b 39182	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ OP ∧ 𝑣 ∈ 𝐵 ∧ 𝑡 ∈ 𝐵) → (𝑣(le‘𝐾)𝑡 ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣)))
103	61, 100, 101, 102	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (𝑣(le‘𝐾)𝑡 ↔ ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣)))
104	99, 103	imbi12d 344	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → ((∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡) ↔ (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣))))
105	104	ralbidva 3174	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡) ↔ ∀𝑡 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑡)(le‘𝐾)𝑧 → ( ⊥ ‘𝑡)(le‘𝐾)( ⊥ ‘𝑣))))
106	78, 105	bitr4d 282	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → (∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)) ↔ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡)))
107	60, 106	anbi12d 632	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ 𝑣 ∈ 𝐵) → ((∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣))) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡))))
108	107	riotabidva 7407	. . . . 5 ⊢ (𝐾 ∈ HL → (℩𝑣 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)))) = (℩𝑣 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡))))
109		ssrab2 4090	. . . . . 6 ⊢ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆} ⊆ 𝐵
110		glbcon.u	. . . . . . 7 ⊢ 𝑈 = (lub‘𝐾)
111		biid 261	. . . . . . 7 ⊢ ((∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡)) ↔ (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡)))
112		simpl 482	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆} ⊆ 𝐵) → 𝐾 ∈ HL)
113		simpr 484	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆} ⊆ 𝐵) → {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆} ⊆ 𝐵)
114	6, 7, 110, 111, 112, 113	lubval 18414	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆} ⊆ 𝐵) → (𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}) = (℩𝑣 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡))))
115	109, 114	mpan2 691	. . . . 5 ⊢ (𝐾 ∈ HL → (𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}) = (℩𝑣 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑣 ∧ ∀𝑡 ∈ 𝐵 (∀𝑢 ∈ {𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}𝑢(le‘𝐾)𝑡 → 𝑣(le‘𝐾)𝑡))))
116	108, 115	eqtr4d 2778	. . . 4 ⊢ (𝐾 ∈ HL → (℩𝑣 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣)))) = (𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}))
117	116	fveq2d 6911	. . 3 ⊢ (𝐾 ∈ HL → ( ⊥ ‘(℩𝑣 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆} ( ⊥ ‘𝑣)(le‘𝐾)𝑧 ∧ ∀𝑤 ∈ 𝐵 (∀𝑧 ∈ {𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}𝑤(le‘𝐾)𝑧 → 𝑤(le‘𝐾)( ⊥ ‘𝑣))))) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆})))
118	13, 30, 117	3eqtrd 2779	. 2 ⊢ (𝐾 ∈ HL → (𝐺‘{𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝑆}) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆})))
119	5, 118	sylan9eqr 2797	1 ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆})))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068  ∃!wreu 3376  {crab 3433   ∩ cin 3962   ⊆ wss 3963   class class class wbr 5148  ‘cfv 6563  ℩crio 7387  Basecbs 17245  lecple 17305  occoc 17306  lubclub 18367  glbcglb 18368  CLatccla 18556  OPcops 39154  HLchlt 39332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-riotaBAD 38935

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-undef 8297  df-lub 18404  df-glb 18405  df-clat 18557  df-oposet 39158  df-ol 39160  df-oml 39161  df-hlat 39333

This theorem is referenced by: (None)