glbconN

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 df-riota . (Revised by SN, 3-Jan-2025) (New usage is discouraged.)

	Ref	Expression
Hypotheses	glbcon.b	$⊢ B = {Base}_{K}$
	glbcon.u	$⊢ U = lub (K)$
	glbcon.g	$⊢ G = glb (K)$
	glbcon.o	$⊢ \underset{˙}{⊥} = oc (K)$
Assertion	glbconN	$⊢ (K \in HL \land S \subseteq B) \to G (S) = \underset{˙}{⊥} (U (\{x \in B \| \underset{˙}{⊥} (x) \in S\}))$

Proof

Step	Hyp	Ref	Expression
1		glbcon.b	$⊢ B = {Base}_{K}$
2		glbcon.u	$⊢ U = lub (K)$
3		glbcon.g	$⊢ G = glb (K)$
4		glbcon.o	$⊢ \underset{˙}{⊥} = oc (K)$
5		sseqin2	$⊢ S \subseteq B \leftrightarrow B \cap S = S$
6	5	biimpi	$⊢ S \subseteq B \to B \cap S = S$
7		dfin5	$⊢ B \cap S = \{x \in B \| x \in S\}$
8	6 7	eqtr3di	$⊢ S \subseteq B \to S = \{x \in B \| x \in S\}$
9	8	fveq2d	$⊢ S \subseteq B \to G (S) = G (\{x \in B \| x \in S\})$
10		eqid	$⊢ \leq_{K} = \leq_{K}$
11		biid	$⊢ (\forall z \in \{x \in B \| x \in S\} y \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} y)) \leftrightarrow (\forall z \in \{x \in B \| x \in S\} y \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} y))$
12		id	$⊢ K \in HL \to K \in HL$
13		ssrab2	$⊢ \{x \in B \| x \in S\} \subseteq B$
14	13	a1i	$⊢ K \in HL \to \{x \in B \| x \in S\} \subseteq B$
15	1 10 3 11 12 14	glbval	$⊢ K \in HL \to G (\{x \in B \| x \in S\}) = (ι y \in B \| (\forall z \in \{x \in B \| x \in S\} y \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} y)))$
16		hlop	$⊢ K \in HL \to K \in OP$
17		hlclat	$⊢ K \in HL \to K \in CLat$
18	1 3	clatglbcl2	$⊢ (K \in CLat \land \{x \in B \| x \in S\} \subseteq B) \to \{x \in B \| x \in S\} \in dom G$
19	17 14 18	syl2anc	$⊢ K \in HL \to \{x \in B \| x \in S\} \in dom G$
20	1 10 3 11 12 19	glbeu	$⊢ K \in HL \to \exists! y \in B (\forall z \in \{x \in B \| x \in S\} y \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} y))$
21		breq1	$⊢ y = \underset{˙}{⊥} (v) \to (y \leq_{K} z \leftrightarrow \underset{˙}{⊥} (v) \leq_{K} z)$
22	21	ralbidv	$⊢ y = \underset{˙}{⊥} (v) \to (\forall z \in \{x \in B \| x \in S\} y \leq_{K} z \leftrightarrow \forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (v) \leq_{K} z)$
23		breq2	$⊢ y = \underset{˙}{⊥} (v) \to (w \leq_{K} y \leftrightarrow w \leq_{K} \underset{˙}{⊥} (v))$
24	23	imbi2d	$⊢ y = \underset{˙}{⊥} (v) \to ((\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} y) \leftrightarrow (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v)))$
25	24	ralbidv	$⊢ y = \underset{˙}{⊥} (v) \to (\forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} y) \leftrightarrow \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v)))$
26	22 25	anbi12d	$⊢ y = \underset{˙}{⊥} (v) \to ((\forall z \in \{x \in B \| x \in S\} y \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} y)) \leftrightarrow (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (v) \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v))))$
27	1 4 26	riotaocN	$⊢ (K \in OP \land \exists! y \in B (\forall z \in \{x \in B \| x \in S\} y \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} y))) \to (ι y \in B \| (\forall z \in \{x \in B \| x \in S\} y \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} y))) = \underset{˙}{⊥} ((ι v \in B \| (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (v) \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v)))))$
28	16 20 27	syl2anc	$⊢ K \in HL \to (ι y \in B \| (\forall z \in \{x \in B \| x \in S\} y \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} y))) = \underset{˙}{⊥} ((ι v \in B \| (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (v) \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v)))))$
29	16	ad2antrr	$⊢ ((K \in HL \land v \in B) \land u \in B) \to K \in OP$
30	1 4	opoccl	$⊢ (K \in OP \land u \in B) \to \underset{˙}{⊥} (u) \in B$
31	29 30	sylancom	$⊢ ((K \in HL \land v \in B) \land u \in B) \to \underset{˙}{⊥} (u) \in B$
32	16	ad2antrr	$⊢ ((K \in HL \land v \in B) \land z \in B) \to K \in OP$
33	1 4	opoccl	$⊢ (K \in OP \land z \in B) \to \underset{˙}{⊥} (z) \in B$
34	32 33	sylancom	$⊢ ((K \in HL \land v \in B) \land z \in B) \to \underset{˙}{⊥} (z) \in B$
35	1 4	opococ	$⊢ (K \in OP \land z \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (z)) = z$
36	32 35	sylancom	$⊢ ((K \in HL \land v \in B) \land z \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (z)) = z$
37	36	eqcomd	$⊢ ((K \in HL \land v \in B) \land z \in B) \to z = \underset{˙}{⊥} (\underset{˙}{⊥} (z))$
38		fveq2	$⊢ u = \underset{˙}{⊥} (z) \to \underset{˙}{⊥} (u) = \underset{˙}{⊥} (\underset{˙}{⊥} (z))$
39	38	rspceeqv	$⊢ (\underset{˙}{⊥} (z) \in B \land z = \underset{˙}{⊥} (\underset{˙}{⊥} (z))) \to \exists u \in B z = \underset{˙}{⊥} (u)$
40	34 37 39	syl2anc	$⊢ ((K \in HL \land v \in B) \land z \in B) \to \exists u \in B z = \underset{˙}{⊥} (u)$
41		eleq1	$⊢ z = \underset{˙}{⊥} (u) \to (z \in S \leftrightarrow \underset{˙}{⊥} (u) \in S)$
42		breq2	$⊢ z = \underset{˙}{⊥} (u) \to (\underset{˙}{⊥} (v) \leq_{K} z \leftrightarrow \underset{˙}{⊥} (v) \leq_{K} \underset{˙}{⊥} (u))$
43	41 42	imbi12d	$⊢ z = \underset{˙}{⊥} (u) \to ((z \in S \to \underset{˙}{⊥} (v) \leq_{K} z) \leftrightarrow (\underset{˙}{⊥} (u) \in S \to \underset{˙}{⊥} (v) \leq_{K} \underset{˙}{⊥} (u)))$
44	43	adantl	$⊢ ((K \in HL \land v \in B) \land z = \underset{˙}{⊥} (u)) \to ((z \in S \to \underset{˙}{⊥} (v) \leq_{K} z) \leftrightarrow (\underset{˙}{⊥} (u) \in S \to \underset{˙}{⊥} (v) \leq_{K} \underset{˙}{⊥} (u)))$
45	31 40 44	ralxfrd	$⊢ (K \in HL \land v \in B) \to (\forall z \in B (z \in S \to \underset{˙}{⊥} (v) \leq_{K} z) \leftrightarrow \forall u \in B (\underset{˙}{⊥} (u) \in S \to \underset{˙}{⊥} (v) \leq_{K} \underset{˙}{⊥} (u)))$
46		simpr	$⊢ ((K \in HL \land v \in B) \land u \in B) \to u \in B$
47		simplr	$⊢ ((K \in HL \land v \in B) \land u \in B) \to v \in B$
48	1 10 4	oplecon3b	$⊢ (K \in OP \land u \in B \land v \in B) \to (u \leq_{K} v \leftrightarrow \underset{˙}{⊥} (v) \leq_{K} \underset{˙}{⊥} (u))$
49	29 46 47 48	syl3anc	$⊢ ((K \in HL \land v \in B) \land u \in B) \to (u \leq_{K} v \leftrightarrow \underset{˙}{⊥} (v) \leq_{K} \underset{˙}{⊥} (u))$
50	49	imbi2d	$⊢ ((K \in HL \land v \in B) \land u \in B) \to ((\underset{˙}{⊥} (u) \in S \to u \leq_{K} v) \leftrightarrow (\underset{˙}{⊥} (u) \in S \to \underset{˙}{⊥} (v) \leq_{K} \underset{˙}{⊥} (u)))$
51	50	ralbidva	$⊢ (K \in HL \land v \in B) \to (\forall u \in B (\underset{˙}{⊥} (u) \in S \to u \leq_{K} v) \leftrightarrow \forall u \in B (\underset{˙}{⊥} (u) \in S \to \underset{˙}{⊥} (v) \leq_{K} \underset{˙}{⊥} (u)))$
52	45 51	bitr4d	$⊢ (K \in HL \land v \in B) \to (\forall z \in B (z \in S \to \underset{˙}{⊥} (v) \leq_{K} z) \leftrightarrow \forall u \in B (\underset{˙}{⊥} (u) \in S \to u \leq_{K} v))$
53		eleq1	$⊢ x = z \to (x \in S \leftrightarrow z \in S)$
54	53	ralrab	$⊢ \forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (v) \leq_{K} z \leftrightarrow \forall z \in B (z \in S \to \underset{˙}{⊥} (v) \leq_{K} z)$
55		fveq2	$⊢ x = u \to \underset{˙}{⊥} (x) = \underset{˙}{⊥} (u)$
56	55	eleq1d	$⊢ x = u \to (\underset{˙}{⊥} (x) \in S \leftrightarrow \underset{˙}{⊥} (u) \in S)$
57	56	ralrab	$⊢ \forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} v \leftrightarrow \forall u \in B (\underset{˙}{⊥} (u) \in S \to u \leq_{K} v)$
58	52 54 57	3bitr4g	$⊢ (K \in HL \land v \in B) \to (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (v) \leq_{K} z \leftrightarrow \forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} v)$
59	16	ad2antrr	$⊢ ((K \in HL \land v \in B) \land t \in B) \to K \in OP$
60	1 4	opoccl	$⊢ (K \in OP \land t \in B) \to \underset{˙}{⊥} (t) \in B$
61	59 60	sylancom	$⊢ ((K \in HL \land v \in B) \land t \in B) \to \underset{˙}{⊥} (t) \in B$
62	16	ad2antrr	$⊢ ((K \in HL \land v \in B) \land w \in B) \to K \in OP$
63	1 4	opoccl	$⊢ (K \in OP \land w \in B) \to \underset{˙}{⊥} (w) \in B$
64	62 63	sylancom	$⊢ ((K \in HL \land v \in B) \land w \in B) \to \underset{˙}{⊥} (w) \in B$
65	1 4	opococ	$⊢ (K \in OP \land w \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (w)) = w$
66	62 65	sylancom	$⊢ ((K \in HL \land v \in B) \land w \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (w)) = w$
67	66	eqcomd	$⊢ ((K \in HL \land v \in B) \land w \in B) \to w = \underset{˙}{⊥} (\underset{˙}{⊥} (w))$
68		fveq2	$⊢ t = \underset{˙}{⊥} (w) \to \underset{˙}{⊥} (t) = \underset{˙}{⊥} (\underset{˙}{⊥} (w))$
69	68	rspceeqv	$⊢ (\underset{˙}{⊥} (w) \in B \land w = \underset{˙}{⊥} (\underset{˙}{⊥} (w))) \to \exists t \in B w = \underset{˙}{⊥} (t)$
70	64 67 69	syl2anc	$⊢ ((K \in HL \land v \in B) \land w \in B) \to \exists t \in B w = \underset{˙}{⊥} (t)$
71		breq1	$⊢ w = \underset{˙}{⊥} (t) \to (w \leq_{K} z \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} z)$
72	71	ralbidv	$⊢ w = \underset{˙}{⊥} (t) \to (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \leftrightarrow \forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (t) \leq_{K} z)$
73		breq1	$⊢ w = \underset{˙}{⊥} (t) \to (w \leq_{K} \underset{˙}{⊥} (v) \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (v))$
74	72 73	imbi12d	$⊢ w = \underset{˙}{⊥} (t) \to ((\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v)) \leftrightarrow (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (t) \leq_{K} z \to \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (v)))$
75	74	adantl	$⊢ ((K \in HL \land v \in B) \land w = \underset{˙}{⊥} (t)) \to ((\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v)) \leftrightarrow (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (t) \leq_{K} z \to \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (v)))$
76	61 70 75	ralxfrd	$⊢ (K \in HL \land v \in B) \to (\forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v)) \leftrightarrow \forall t \in B (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (t) \leq_{K} z \to \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (v)))$
77	16	ad3antrrr	$⊢ (((K \in HL \land v \in B) \land t \in B) \land u \in B) \to K \in OP$
78		simpr	$⊢ (((K \in HL \land v \in B) \land t \in B) \land u \in B) \to u \in B$
79		simplr	$⊢ (((K \in HL \land v \in B) \land t \in B) \land u \in B) \to t \in B$
80	1 10 4	oplecon3b	$⊢ (K \in OP \land u \in B \land t \in B) \to (u \leq_{K} t \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (u))$
81	77 78 79 80	syl3anc	$⊢ (((K \in HL \land v \in B) \land t \in B) \land u \in B) \to (u \leq_{K} t \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (u))$
82	81	imbi2d	$⊢ (((K \in HL \land v \in B) \land t \in B) \land u \in B) \to ((\underset{˙}{⊥} (u) \in S \to u \leq_{K} t) \leftrightarrow (\underset{˙}{⊥} (u) \in S \to \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (u)))$
83	82	ralbidva	$⊢ ((K \in HL \land v \in B) \land t \in B) \to (\forall u \in B (\underset{˙}{⊥} (u) \in S \to u \leq_{K} t) \leftrightarrow \forall u \in B (\underset{˙}{⊥} (u) \in S \to \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (u)))$
84	77 30	sylancom	$⊢ (((K \in HL \land v \in B) \land t \in B) \land u \in B) \to \underset{˙}{⊥} (u) \in B$
85	16	ad3antrrr	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z \in B) \to K \in OP$
86	85 33	sylancom	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z \in B) \to \underset{˙}{⊥} (z) \in B$
87	85 35	sylancom	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (z)) = z$
88	87	eqcomd	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z \in B) \to z = \underset{˙}{⊥} (\underset{˙}{⊥} (z))$
89	86 88 39	syl2anc	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z \in B) \to \exists u \in B z = \underset{˙}{⊥} (u)$
90		breq2	$⊢ z = \underset{˙}{⊥} (u) \to (\underset{˙}{⊥} (t) \leq_{K} z \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (u))$
91	41 90	imbi12d	$⊢ z = \underset{˙}{⊥} (u) \to ((z \in S \to \underset{˙}{⊥} (t) \leq_{K} z) \leftrightarrow (\underset{˙}{⊥} (u) \in S \to \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (u)))$
92	91	adantl	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z = \underset{˙}{⊥} (u)) \to ((z \in S \to \underset{˙}{⊥} (t) \leq_{K} z) \leftrightarrow (\underset{˙}{⊥} (u) \in S \to \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (u)))$
93	84 89 92	ralxfrd	$⊢ ((K \in HL \land v \in B) \land t \in B) \to (\forall z \in B (z \in S \to \underset{˙}{⊥} (t) \leq_{K} z) \leftrightarrow \forall u \in B (\underset{˙}{⊥} (u) \in S \to \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (u)))$
94	83 93	bitr4d	$⊢ ((K \in HL \land v \in B) \land t \in B) \to (\forall u \in B (\underset{˙}{⊥} (u) \in S \to u \leq_{K} t) \leftrightarrow \forall z \in B (z \in S \to \underset{˙}{⊥} (t) \leq_{K} z))$
95	56	ralrab	$⊢ \forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \leftrightarrow \forall u \in B (\underset{˙}{⊥} (u) \in S \to u \leq_{K} t)$
96	53	ralrab	$⊢ \forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (t) \leq_{K} z \leftrightarrow \forall z \in B (z \in S \to \underset{˙}{⊥} (t) \leq_{K} z)$
97	94 95 96	3bitr4g	$⊢ ((K \in HL \land v \in B) \land t \in B) \to (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \leftrightarrow \forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (t) \leq_{K} z)$
98		simplr	$⊢ ((K \in HL \land v \in B) \land t \in B) \to v \in B$
99		simpr	$⊢ ((K \in HL \land v \in B) \land t \in B) \to t \in B$
100	1 10 4	oplecon3b	$⊢ (K \in OP \land v \in B \land t \in B) \to (v \leq_{K} t \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (v))$
101	59 98 99 100	syl3anc	$⊢ ((K \in HL \land v \in B) \land t \in B) \to (v \leq_{K} t \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (v))$
102	97 101	imbi12d	$⊢ ((K \in HL \land v \in B) \land t \in B) \to ((\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \to v \leq_{K} t) \leftrightarrow (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (t) \leq_{K} z \to \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (v)))$
103	102	ralbidva	$⊢ (K \in HL \land v \in B) \to (\forall t \in B (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \to v \leq_{K} t) \leftrightarrow \forall t \in B (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (t) \leq_{K} z \to \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (v)))$
104	76 103	bitr4d	$⊢ (K \in HL \land v \in B) \to (\forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v)) \leftrightarrow \forall t \in B (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \to v \leq_{K} t))$
105	58 104	anbi12d	$⊢ (K \in HL \land v \in B) \to ((\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (v) \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v))) \leftrightarrow (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} v \land \forall t \in B (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \to v \leq_{K} t)))$
106	105	riotabidva	$⊢ K \in HL \to (ι v \in B \| (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (v) \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v)))) = (ι v \in B \| (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} v \land \forall t \in B (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \to v \leq_{K} t)))$
107		ssrab2	$⊢ \{x \in B \| \underset{˙}{⊥} (x) \in S\} \subseteq B$
108		biid	$⊢ (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} v \land \forall t \in B (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \to v \leq_{K} t)) \leftrightarrow (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} v \land \forall t \in B (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \to v \leq_{K} t))$
109		simpl	$⊢ (K \in HL \land \{x \in B \| \underset{˙}{⊥} (x) \in S\} \subseteq B) \to K \in HL$
110		simpr	$⊢ (K \in HL \land \{x \in B \| \underset{˙}{⊥} (x) \in S\} \subseteq B) \to \{x \in B \| \underset{˙}{⊥} (x) \in S\} \subseteq B$
111	1 10 2 108 109 110	lubval	$⊢ (K \in HL \land \{x \in B \| \underset{˙}{⊥} (x) \in S\} \subseteq B) \to U (\{x \in B \| \underset{˙}{⊥} (x) \in S\}) = (ι v \in B \| (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} v \land \forall t \in B (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \to v \leq_{K} t)))$
112	107 111	mpan2	$⊢ K \in HL \to U (\{x \in B \| \underset{˙}{⊥} (x) \in S\}) = (ι v \in B \| (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} v \land \forall t \in B (\forall u \in \{x \in B \| \underset{˙}{⊥} (x) \in S\} u \leq_{K} t \to v \leq_{K} t)))$
113	106 112	eqtr4d	$⊢ K \in HL \to (ι v \in B \| (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (v) \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v)))) = U (\{x \in B \| \underset{˙}{⊥} (x) \in S\})$
114	113	fveq2d	$⊢ K \in HL \to \underset{˙}{⊥} ((ι v \in B \| (\forall z \in \{x \in B \| x \in S\} \underset{˙}{⊥} (v) \leq_{K} z \land \forall w \in B (\forall z \in \{x \in B \| x \in S\} w \leq_{K} z \to w \leq_{K} \underset{˙}{⊥} (v))))) = \underset{˙}{⊥} (U (\{x \in B \| \underset{˙}{⊥} (x) \in S\}))$
115	15 28 114	3eqtrd	$⊢ K \in HL \to G (\{x \in B \| x \in S\}) = \underset{˙}{⊥} (U (\{x \in B \| \underset{˙}{⊥} (x) \in S\}))$
116	9 115	sylan9eqr	$⊢ (K \in HL \land S \subseteq B) \to G (S) = \underset{˙}{⊥} (U (\{x \in B \| \underset{˙}{⊥} (x) \in S\}))$

Metamath Proof Explorer

Theorem glbconN

Proof