Theorem 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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	glbcon.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	glbcon.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
	glbcon.o	⊢ ⊥ = ( oc ‘ 𝐾 )
Assertion	glbconxN	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		glbcon.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		glbcon.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
3		glbcon.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		glbcon.o	⊢ ⊥ = ( oc ‘ 𝐾 )
5		vex	⊢ 𝑦 ∈ V
6		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑆 ↔ 𝑦 = 𝑆 ) )
7	6	rexbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 ↔ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 ) )
8	5 7	elab	⊢ ( 𝑦 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ↔ ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 )
9		nfra1	⊢ Ⅎ 𝑖 ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵
10		nfv	⊢ Ⅎ 𝑖 𝑦 ∈ 𝐵
11		rsp	⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( 𝑖 ∈ 𝐼 → 𝑆 ∈ 𝐵 ) )
12		eleq1a	⊢ ( 𝑆 ∈ 𝐵 → ( 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) )
13	11 12	syl6	⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( 𝑖 ∈ 𝐼 → ( 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) ) )
14	9 10 13	rexlimd	⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( ∃ 𝑖 ∈ 𝐼 𝑦 = 𝑆 → 𝑦 ∈ 𝐵 ) )
15	8 14	syl5bi	⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → ( 𝑦 ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } → 𝑦 ∈ 𝐵 ) )
16	15	ssrdv	⊢ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 → { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ⊆ 𝐵 )
17	1 2 3 4	glbconN	⊢ ( ( 𝐾 ∈ HL ∧ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ⊆ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) ) )
18	16 17	sylan2	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) ) )
19		fvex	⊢ ( ⊥ ‘ 𝑦 ) ∈ V
20		eqeq1	⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( 𝑥 = 𝑆 ↔ ( ⊥ ‘ 𝑦 ) = 𝑆 ) )
21	20	rexbidv	⊢ ( 𝑥 = ( ⊥ ‘ 𝑦 ) → ( ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 ↔ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) )
22	19 21	elab	⊢ ( ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ↔ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 )
23	22	rabbii	⊢ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } = { 𝑦 ∈ 𝐵 ∣ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 }
24		df-rab	⊢ { 𝑦 ∈ 𝐵 ∣ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) }
25	23 24	eqtri	⊢ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) }
26		nfv	⊢ Ⅎ 𝑖 𝐾 ∈ HL
27	26 9	nfan	⊢ Ⅎ 𝑖 ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 )
28		rspa	⊢ ( ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼 ) → 𝑆 ∈ 𝐵 )
29		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
30	1 4	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑆 ∈ 𝐵 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐵 )
31	29 30	sylan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( ⊥ ‘ 𝑆 ) ∈ 𝐵 )
32		eleq1a	⊢ ( ( ⊥ ‘ 𝑆 ) ∈ 𝐵 → ( 𝑦 = ( ⊥ ‘ 𝑆 ) → 𝑦 ∈ 𝐵 ) )
33	31 32	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) → 𝑦 ∈ 𝐵 ) )
34	33	pm4.71rd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 = ( ⊥ ‘ 𝑆 ) ) ) )
35	1 4	opcon2b	⊢ ( ( 𝐾 ∈ OP ∧ 𝑆 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ 𝑦 = ( ⊥ ‘ 𝑆 ) ) )
36	29 35	syl3an1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ 𝑦 = ( ⊥ ‘ 𝑆 ) ) )
37	36	3expa	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ 𝑦 = ( ⊥ ‘ 𝑆 ) ) )
38		eqcom	⊢ ( 𝑆 = ( ⊥ ‘ 𝑦 ) ↔ ( ⊥ ‘ 𝑦 ) = 𝑆 )
39	37 38	bitr3di	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( ⊥ ‘ 𝑦 ) = 𝑆 ) )
40	39	pm5.32da	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 = ( ⊥ ‘ 𝑆 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) )
41	34 40	bitrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) )
42	28 41	sylan2	⊢ ( ( 𝐾 ∈ HL ∧ ( ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼 ) ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) )
43	42	anassrs	⊢ ( ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) )
44	27 43	rexbida	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ∃ 𝑖 ∈ 𝐼 ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ) )
45		r19.42v	⊢ ( ∃ 𝑖 ∈ 𝐼 ( 𝑦 ∈ 𝐵 ∧ ( ⊥ ‘ 𝑦 ) = 𝑆 ) ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) )
46	44 45	bitr2di	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) ) )
47	46	abbidv	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) } = { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) } )
48		eqeq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ 𝑥 = ( ⊥ ‘ 𝑆 ) ) )
49	48	rexbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) ) )
50	49	cbvabv	⊢ { 𝑦 ∣ ∃ 𝑖 ∈ 𝐼 𝑦 = ( ⊥ ‘ 𝑆 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) }
51	47 50	eqtrdi	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑖 ∈ 𝐼 ( ⊥ ‘ 𝑦 ) = 𝑆 ) } = { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } )
52	25 51	syl5eq	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } = { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } )
53	52	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) = ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) )
54	53	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( ⊥ ‘ ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ ( ⊥ ‘ 𝑦 ) ∈ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } } ) ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) ) )
55	18 54	eqtrd	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ) → ( 𝐺 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝑆 } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘ 𝑆 ) } ) ) )