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 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	clatglbcl	$⊢ (K \in CLat \land \{x \in B \| x \in S\} \subseteq B) \to G (\{x \in B \| x \in S\}) \in B$
19	17 13 18	sylancl	$⊢ K \in HL \to G (\{x \in B \| x \in S\}) \in B$
20	15 19	eqeltrrd	$⊢ 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))) \in B$
21	1	fvexi	$⊢ B \in V$
22	21	riotaclbBAD	$⊢ \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)) \leftrightarrow (ι 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))) \in B$
23	20 22	sylibr	$⊢ 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))$
24		breq1	$⊢ y = \underset{˙}{⊥} (v) \to (y \leq_{K} z \leftrightarrow \underset{˙}{⊥} (v) \leq_{K} z)$
25	24	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)$
26		breq2	$⊢ y = \underset{˙}{⊥} (v) \to (w \leq_{K} y \leftrightarrow w \leq_{K} \underset{˙}{⊥} (v))$
27	26	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)))$
28	27	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)))$
29	25 28	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))))$
30	1 4 29	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)))))$
31	16 23 30	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)))))$
32	16	ad2antrr	$⊢ ((K \in HL \land v \in B) \land u \in B) \to K \in OP$
33	1 4	opoccl	$⊢ (K \in OP \land u \in B) \to \underset{˙}{⊥} (u) \in B$
34	32 33	sylancom	$⊢ ((K \in HL \land v \in B) \land u \in B) \to \underset{˙}{⊥} (u) \in B$
35	16	ad2antrr	$⊢ ((K \in HL \land v \in B) \land z \in B) \to K \in OP$
36	1 4	opoccl	$⊢ (K \in OP \land z \in B) \to \underset{˙}{⊥} (z) \in B$
37	35 36	sylancom	$⊢ ((K \in HL \land v \in B) \land z \in B) \to \underset{˙}{⊥} (z) \in B$
38	1 4	opococ	$⊢ (K \in OP \land z \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (z)) = z$
39	35 38	sylancom	$⊢ ((K \in HL \land v \in B) \land z \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (z)) = z$
40	39	eqcomd	$⊢ ((K \in HL \land v \in B) \land z \in B) \to z = \underset{˙}{⊥} (\underset{˙}{⊥} (z))$
41		fveq2	$⊢ u = \underset{˙}{⊥} (z) \to \underset{˙}{⊥} (u) = \underset{˙}{⊥} (\underset{˙}{⊥} (z))$
42	41	rspceeqv	$⊢ (\underset{˙}{⊥} (z) \in B \land z = \underset{˙}{⊥} (\underset{˙}{⊥} (z))) \to \exists u \in B z = \underset{˙}{⊥} (u)$
43	37 40 42	syl2anc	$⊢ ((K \in HL \land v \in B) \land z \in B) \to \exists u \in B z = \underset{˙}{⊥} (u)$
44		eleq1	$⊢ z = \underset{˙}{⊥} (u) \to (z \in S \leftrightarrow \underset{˙}{⊥} (u) \in S)$
45		breq2	$⊢ z = \underset{˙}{⊥} (u) \to (\underset{˙}{⊥} (v) \leq_{K} z \leftrightarrow \underset{˙}{⊥} (v) \leq_{K} \underset{˙}{⊥} (u))$
46	44 45	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)))$
47	46	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)))$
48	34 43 47	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)))$
49		simpr	$⊢ ((K \in HL \land v \in B) \land u \in B) \to u \in B$
50		simplr	$⊢ ((K \in HL \land v \in B) \land u \in B) \to v \in B$
51	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))$
52	32 49 50 51	syl3anc	$⊢ ((K \in HL \land v \in B) \land u \in B) \to (u \leq_{K} v \leftrightarrow \underset{˙}{⊥} (v) \leq_{K} \underset{˙}{⊥} (u))$
53	52	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)))$
54	53	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)))$
55	48 54	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))$
56		eleq1	$⊢ x = z \to (x \in S \leftrightarrow z \in S)$
57	56	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)$
58		fveq2	$⊢ x = u \to \underset{˙}{⊥} (x) = \underset{˙}{⊥} (u)$
59	58	eleq1d	$⊢ x = u \to (\underset{˙}{⊥} (x) \in S \leftrightarrow \underset{˙}{⊥} (u) \in S)$
60	59	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)$
61	55 57 60	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)$
62	16	ad2antrr	$⊢ ((K \in HL \land v \in B) \land t \in B) \to K \in OP$
63	1 4	opoccl	$⊢ (K \in OP \land t \in B) \to \underset{˙}{⊥} (t) \in B$
64	62 63	sylancom	$⊢ ((K \in HL \land v \in B) \land t \in B) \to \underset{˙}{⊥} (t) \in B$
65	16	ad2antrr	$⊢ ((K \in HL \land v \in B) \land w \in B) \to K \in OP$
66	1 4	opoccl	$⊢ (K \in OP \land w \in B) \to \underset{˙}{⊥} (w) \in B$
67	65 66	sylancom	$⊢ ((K \in HL \land v \in B) \land w \in B) \to \underset{˙}{⊥} (w) \in B$
68	1 4	opococ	$⊢ (K \in OP \land w \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (w)) = w$
69	65 68	sylancom	$⊢ ((K \in HL \land v \in B) \land w \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (w)) = w$
70	69	eqcomd	$⊢ ((K \in HL \land v \in B) \land w \in B) \to w = \underset{˙}{⊥} (\underset{˙}{⊥} (w))$
71		fveq2	$⊢ t = \underset{˙}{⊥} (w) \to \underset{˙}{⊥} (t) = \underset{˙}{⊥} (\underset{˙}{⊥} (w))$
72	71	rspceeqv	$⊢ (\underset{˙}{⊥} (w) \in B \land w = \underset{˙}{⊥} (\underset{˙}{⊥} (w))) \to \exists t \in B w = \underset{˙}{⊥} (t)$
73	67 70 72	syl2anc	$⊢ ((K \in HL \land v \in B) \land w \in B) \to \exists t \in B w = \underset{˙}{⊥} (t)$
74		breq1	$⊢ w = \underset{˙}{⊥} (t) \to (w \leq_{K} z \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} z)$
75	74	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)$
76		breq1	$⊢ w = \underset{˙}{⊥} (t) \to (w \leq_{K} \underset{˙}{⊥} (v) \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (v))$
77	75 76	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)))$
78	77	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)))$
79	64 73 78	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)))$
80	16	ad3antrrr	$⊢ (((K \in HL \land v \in B) \land t \in B) \land u \in B) \to K \in OP$
81		simpr	$⊢ (((K \in HL \land v \in B) \land t \in B) \land u \in B) \to u \in B$
82		simplr	$⊢ (((K \in HL \land v \in B) \land t \in B) \land u \in B) \to t \in B$
83	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))$
84	80 81 82 83	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))$
85	84	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)))$
86	85	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)))$
87	80 33	sylancom	$⊢ (((K \in HL \land v \in B) \land t \in B) \land u \in B) \to \underset{˙}{⊥} (u) \in B$
88	16	ad3antrrr	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z \in B) \to K \in OP$
89	88 36	sylancom	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z \in B) \to \underset{˙}{⊥} (z) \in B$
90	88 38	sylancom	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z \in B) \to \underset{˙}{⊥} (\underset{˙}{⊥} (z)) = z$
91	90	eqcomd	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z \in B) \to z = \underset{˙}{⊥} (\underset{˙}{⊥} (z))$
92	89 91 42	syl2anc	$⊢ (((K \in HL \land v \in B) \land t \in B) \land z \in B) \to \exists u \in B z = \underset{˙}{⊥} (u)$
93		breq2	$⊢ z = \underset{˙}{⊥} (u) \to (\underset{˙}{⊥} (t) \leq_{K} z \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (u))$
94	44 93	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)))$
95	94	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)))$
96	87 92 95	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)))$
97	86 96	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))$
98	59	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)$
99	56	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)$
100	97 98 99	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)$
101		simplr	$⊢ ((K \in HL \land v \in B) \land t \in B) \to v \in B$
102		simpr	$⊢ ((K \in HL \land v \in B) \land t \in B) \to t \in B$
103	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))$
104	62 101 102 103	syl3anc	$⊢ ((K \in HL \land v \in B) \land t \in B) \to (v \leq_{K} t \leftrightarrow \underset{˙}{⊥} (t) \leq_{K} \underset{˙}{⊥} (v))$
105	100 104	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)))$
106	105	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)))$
107	79 106	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))$
108	61 107	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)))$
109	108	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)))$
110		ssrab2	$⊢ \{x \in B \| \underset{˙}{⊥} (x) \in S\} \subseteq B$
111		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))$
112		simpl	$⊢ (K \in HL \land \{x \in B \| \underset{˙}{⊥} (x) \in S\} \subseteq B) \to K \in HL$
113		simpr	$⊢ (K \in HL \land \{x \in B \| \underset{˙}{⊥} (x) \in S\} \subseteq B) \to \{x \in B \| \underset{˙}{⊥} (x) \in S\} \subseteq B$
114	1 10 2 111 112 113	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)))$
115	110 114	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)))$
116	109 115	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\})$
117	116	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\}))$
118	15 31 117	3eqtrd	$⊢ K \in HL \to G (\{x \in B \| x \in S\}) = \underset{˙}{⊥} (U (\{x \in B \| \underset{˙}{⊥} (x) \in S\}))$
119	9 118	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