glbconxN

Description: De Morgan's law for GLB and LUB. Index-set version of glbconN , where we read S as S ( i ) . (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	glbconxN	$⊢ (K \in HL \land \forall i \in I S \in B) \to G (\{x \| \exists i \in I x = S\}) = \underset{˙}{⊥} (U (\{x \| \exists i \in I x = \underset{˙}{⊥} (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		vex	$⊢ y \in V$
6		eqeq1	$⊢ x = y \to (x = S \leftrightarrow y = S)$
7	6	rexbidv	$⊢ x = y \to (\exists i \in I x = S \leftrightarrow \exists i \in I y = S)$
8	5 7	elab	$⊢ y \in \{x \| \exists i \in I x = S\} \leftrightarrow \exists i \in I y = S$
9		nfra1	$⊢ Ⅎ i \forall i \in I S \in B$
10		nfv	$⊢ Ⅎ i y \in B$
11		rsp	$⊢ \forall i \in I S \in B \to (i \in I \to S \in B)$
12		eleq1a	$⊢ S \in B \to (y = S \to y \in B)$
13	11 12	syl6	$⊢ \forall i \in I S \in B \to (i \in I \to (y = S \to y \in B))$
14	9 10 13	rexlimd	$⊢ \forall i \in I S \in B \to (\exists i \in I y = S \to y \in B)$
15	8 14	syl5bi	$⊢ \forall i \in I S \in B \to (y \in \{x \| \exists i \in I x = S\} \to y \in B)$
16	15	ssrdv	$⊢ \forall i \in I S \in B \to \{x \| \exists i \in I x = S\} \subseteq B$
17	1 2 3 4	glbconN	$⊢ (K \in HL \land \{x \| \exists i \in I x = S\} \subseteq B) \to G (\{x \| \exists i \in I x = S\}) = \underset{˙}{⊥} (U (\{y \in B \| \underset{˙}{⊥} (y) \in \{x \| \exists i \in I x = S\}\}))$
18	16 17	sylan2	$⊢ (K \in HL \land \forall i \in I S \in B) \to G (\{x \| \exists i \in I x = S\}) = \underset{˙}{⊥} (U (\{y \in B \| \underset{˙}{⊥} (y) \in \{x \| \exists i \in I x = S\}\}))$
19		fvex	$⊢ \underset{˙}{⊥} (y) \in V$
20		eqeq1	$⊢ x = \underset{˙}{⊥} (y) \to (x = S \leftrightarrow \underset{˙}{⊥} (y) = S)$
21	20	rexbidv	$⊢ x = \underset{˙}{⊥} (y) \to (\exists i \in I x = S \leftrightarrow \exists i \in I \underset{˙}{⊥} (y) = S)$
22	19 21	elab	$⊢ \underset{˙}{⊥} (y) \in \{x \| \exists i \in I x = S\} \leftrightarrow \exists i \in I \underset{˙}{⊥} (y) = S$
23	22	rabbii	$⊢ \{y \in B \| \underset{˙}{⊥} (y) \in \{x \| \exists i \in I x = S\}\} = \{y \in B \| \exists i \in I \underset{˙}{⊥} (y) = S\}$
24		df-rab	$⊢ \{y \in B \| \exists i \in I \underset{˙}{⊥} (y) = S\} = \{y \| (y \in B \land \exists i \in I \underset{˙}{⊥} (y) = S)\}$
25	23 24	eqtri	$⊢ \{y \in B \| \underset{˙}{⊥} (y) \in \{x \| \exists i \in I x = S\}\} = \{y \| (y \in B \land \exists i \in I \underset{˙}{⊥} (y) = S)\}$
26		nfv	$⊢ Ⅎ i K \in HL$
27	26 9	nfan	$⊢ Ⅎ i (K \in HL \land \forall i \in I S \in B)$
28		rspa	$⊢ (\forall i \in I S \in B \land i \in I) \to S \in B$
29		hlop	$⊢ K \in HL \to K \in OP$
30	1 4	opoccl	$⊢ (K \in OP \land S \in B) \to \underset{˙}{⊥} (S) \in B$
31	29 30	sylan	$⊢ (K \in HL \land S \in B) \to \underset{˙}{⊥} (S) \in B$
32		eleq1a	$⊢ \underset{˙}{⊥} (S) \in B \to (y = \underset{˙}{⊥} (S) \to y \in B)$
33	31 32	syl	$⊢ (K \in HL \land S \in B) \to (y = \underset{˙}{⊥} (S) \to y \in B)$
34	33	pm4.71rd	$⊢ (K \in HL \land S \in B) \to (y = \underset{˙}{⊥} (S) \leftrightarrow (y \in B \land y = \underset{˙}{⊥} (S)))$
35	1 4	opcon2b	$⊢ (K \in OP \land S \in B \land y \in B) \to (S = \underset{˙}{⊥} (y) \leftrightarrow y = \underset{˙}{⊥} (S))$
36	29 35	syl3an1	$⊢ (K \in HL \land S \in B \land y \in B) \to (S = \underset{˙}{⊥} (y) \leftrightarrow y = \underset{˙}{⊥} (S))$
37	36	3expa	$⊢ ((K \in HL \land S \in B) \land y \in B) \to (S = \underset{˙}{⊥} (y) \leftrightarrow y = \underset{˙}{⊥} (S))$
38		eqcom	$⊢ S = \underset{˙}{⊥} (y) \leftrightarrow \underset{˙}{⊥} (y) = S$
39	37 38	bitr3di	$⊢ ((K \in HL \land S \in B) \land y \in B) \to (y = \underset{˙}{⊥} (S) \leftrightarrow \underset{˙}{⊥} (y) = S)$
40	39	pm5.32da	$⊢ (K \in HL \land S \in B) \to ((y \in B \land y = \underset{˙}{⊥} (S)) \leftrightarrow (y \in B \land \underset{˙}{⊥} (y) = S))$
41	34 40	bitrd	$⊢ (K \in HL \land S \in B) \to (y = \underset{˙}{⊥} (S) \leftrightarrow (y \in B \land \underset{˙}{⊥} (y) = S))$
42	28 41	sylan2	$⊢ (K \in HL \land (\forall i \in I S \in B \land i \in I)) \to (y = \underset{˙}{⊥} (S) \leftrightarrow (y \in B \land \underset{˙}{⊥} (y) = S))$
43	42	anassrs	$⊢ ((K \in HL \land \forall i \in I S \in B) \land i \in I) \to (y = \underset{˙}{⊥} (S) \leftrightarrow (y \in B \land \underset{˙}{⊥} (y) = S))$
44	27 43	rexbida	$⊢ (K \in HL \land \forall i \in I S \in B) \to (\exists i \in I y = \underset{˙}{⊥} (S) \leftrightarrow \exists i \in I (y \in B \land \underset{˙}{⊥} (y) = S))$
45		r19.42v	$⊢ \exists i \in I (y \in B \land \underset{˙}{⊥} (y) = S) \leftrightarrow (y \in B \land \exists i \in I \underset{˙}{⊥} (y) = S)$
46	44 45	bitr2di	$⊢ (K \in HL \land \forall i \in I S \in B) \to ((y \in B \land \exists i \in I \underset{˙}{⊥} (y) = S) \leftrightarrow \exists i \in I y = \underset{˙}{⊥} (S))$
47	46	abbidv	$⊢ (K \in HL \land \forall i \in I S \in B) \to \{y \| (y \in B \land \exists i \in I \underset{˙}{⊥} (y) = S)\} = \{y \| \exists i \in I y = \underset{˙}{⊥} (S)\}$
48		eqeq1	$⊢ y = x \to (y = \underset{˙}{⊥} (S) \leftrightarrow x = \underset{˙}{⊥} (S))$
49	48	rexbidv	$⊢ y = x \to (\exists i \in I y = \underset{˙}{⊥} (S) \leftrightarrow \exists i \in I x = \underset{˙}{⊥} (S))$
50	49	cbvabv	$⊢ \{y \| \exists i \in I y = \underset{˙}{⊥} (S)\} = \{x \| \exists i \in I x = \underset{˙}{⊥} (S)\}$
51	47 50	eqtrdi	$⊢ (K \in HL \land \forall i \in I S \in B) \to \{y \| (y \in B \land \exists i \in I \underset{˙}{⊥} (y) = S)\} = \{x \| \exists i \in I x = \underset{˙}{⊥} (S)\}$
52	25 51	eqtrid	$⊢ (K \in HL \land \forall i \in I S \in B) \to \{y \in B \| \underset{˙}{⊥} (y) \in \{x \| \exists i \in I x = S\}\} = \{x \| \exists i \in I x = \underset{˙}{⊥} (S)\}$
53	52	fveq2d	$⊢ (K \in HL \land \forall i \in I S \in B) \to U (\{y \in B \| \underset{˙}{⊥} (y) \in \{x \| \exists i \in I x = S\}\}) = U (\{x \| \exists i \in I x = \underset{˙}{⊥} (S)\})$
54	53	fveq2d	$⊢ (K \in HL \land \forall i \in I S \in B) \to \underset{˙}{⊥} (U (\{y \in B \| \underset{˙}{⊥} (y) \in \{x \| \exists i \in I x = S\}\})) = \underset{˙}{⊥} (U (\{x \| \exists i \in I x = \underset{˙}{⊥} (S)\}))$
55	18 54	eqtrd	$⊢ (K \in HL \land \forall i \in I S \in B) \to G (\{x \| \exists i \in I x = S\}) = \underset{˙}{⊥} (U (\{x \| \exists i \in I x = \underset{˙}{⊥} (S)\}))$

Metamath Proof Explorer

Theorem glbconxN

Proof