ipoglb

Description: The GLB of the inclusion poset. (hypotheses "ipolub.s" and "ipoglb.t" could be eliminated with S e. dom G .) Could be significantly shortened if posglbdg is in quantified form. mrelatglb could potentially be shortened using this. See mrelatglbALT . (Contributed by Zhi Wang, 29-Sep-2024)

	Ref	Expression
Hypotheses	ipolub.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
	ipolub.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	ipolub.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐹 )
	ipoglb.g	⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐼 ) )
	ipoglbdm.t	⊢ ( 𝜑 → 𝑇 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } )
	ipoglb.t	⊢ ( 𝜑 → 𝑇 ∈ 𝐹 )
Assertion	ipoglb	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		ipolub.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
2		ipolub.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		ipolub.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐹 )
4		ipoglb.g	⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐼 ) )
5		ipoglbdm.t	⊢ ( 𝜑 → 𝑇 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } )
6		ipoglb.t	⊢ ( 𝜑 → 𝑇 ∈ 𝐹 )
7		eqid	⊢ ( le ‘ 𝐼 ) = ( le ‘ 𝐼 )
8	1	ipobas	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 = ( Base ‘ 𝐼 ) )
9	2 8	syl	⊢ ( 𝜑 → 𝐹 = ( Base ‘ 𝐼 ) )
10	1	ipopos	⊢ 𝐼 ∈ Poset
11	10	a1i	⊢ ( 𝜑 → 𝐼 ∈ Poset )
12		breq2	⊢ ( 𝑦 = 𝑣 → ( 𝑇 ( le ‘ 𝐼 ) 𝑦 ↔ 𝑇 ( le ‘ 𝐼 ) 𝑣 ) )
13		unilbeu	⊢ ( 𝑇 ∈ 𝐹 → ( ( 𝑇 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) ↔ 𝑇 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } ) )
14	13	biimpar	⊢ ( ( 𝑇 ∈ 𝐹 ∧ 𝑇 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } ) → ( 𝑇 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) )
15	6 5 14	syl2anc	⊢ ( 𝜑 → ( 𝑇 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) )
16	1 2 3 7	ipoglblem	⊢ ( ( 𝜑 ∧ 𝑇 ∈ 𝐹 ) → ( ( 𝑇 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑇 ( le ‘ 𝐼 ) 𝑦 ∧ ∀ 𝑧 ∈ 𝐹 ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐼 ) 𝑦 → 𝑧 ( le ‘ 𝐼 ) 𝑇 ) ) ) )
17	6 16	mpdan	⊢ ( 𝜑 → ( ( 𝑇 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑇 ( le ‘ 𝐼 ) 𝑦 ∧ ∀ 𝑧 ∈ 𝐹 ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐼 ) 𝑦 → 𝑧 ( le ‘ 𝐼 ) 𝑇 ) ) ) )
18	15 17	mpbid	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 𝑇 ( le ‘ 𝐼 ) 𝑦 ∧ ∀ 𝑧 ∈ 𝐹 ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐼 ) 𝑦 → 𝑧 ( le ‘ 𝐼 ) 𝑇 ) ) )
19	18	simpld	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 𝑇 ( le ‘ 𝐼 ) 𝑦 )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → ∀ 𝑦 ∈ 𝑆 𝑇 ( le ‘ 𝐼 ) 𝑦 )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → 𝑣 ∈ 𝑆 )
22	12 20 21	rspcdva	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → 𝑇 ( le ‘ 𝐼 ) 𝑣 )
23		breq1	⊢ ( 𝑧 = 𝑤 → ( 𝑧 ( le ‘ 𝐼 ) 𝑦 ↔ 𝑤 ( le ‘ 𝐼 ) 𝑦 ) )
24	23	ralbidv	⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐼 ) 𝑦 ↔ ∀ 𝑦 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑦 ) )
25		breq2	⊢ ( 𝑦 = 𝑣 → ( 𝑤 ( le ‘ 𝐼 ) 𝑦 ↔ 𝑤 ( le ‘ 𝐼 ) 𝑣 ) )
26	25	cbvralvw	⊢ ( ∀ 𝑦 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑦 ↔ ∀ 𝑣 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 )
27	24 26	bitrdi	⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐼 ) 𝑦 ↔ ∀ 𝑣 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 ) )
28		breq1	⊢ ( 𝑧 = 𝑤 → ( 𝑧 ( le ‘ 𝐼 ) 𝑇 ↔ 𝑤 ( le ‘ 𝐼 ) 𝑇 ) )
29	27 28	imbi12d	⊢ ( 𝑧 = 𝑤 → ( ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐼 ) 𝑦 → 𝑧 ( le ‘ 𝐼 ) 𝑇 ) ↔ ( ∀ 𝑣 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 → 𝑤 ( le ‘ 𝐼 ) 𝑇 ) ) )
30	18	simprd	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐹 ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐼 ) 𝑦 → 𝑧 ( le ‘ 𝐼 ) 𝑇 ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ) → ∀ 𝑧 ∈ 𝐹 ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐼 ) 𝑦 → 𝑧 ( le ‘ 𝐼 ) 𝑇 ) )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ) → 𝑤 ∈ 𝐹 )
33	29 31 32	rspcdva	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ) → ( ∀ 𝑣 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 → 𝑤 ( le ‘ 𝐼 ) 𝑇 ) )
34	33	3impia	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ∧ ∀ 𝑣 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 ) → 𝑤 ( le ‘ 𝐼 ) 𝑇 )
35	7 9 4 11 3 6 22 34	posglbdg	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) = 𝑇 )

Metamath Proof Explorer

Theorem ipoglb

Proof