Theorem ipoglbdm

Description: The domain of the GLB of the inclusion poset. (Contributed by Zhi Wang, 29-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		ipolub.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
2		ipolub.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		ipolub.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐹 )
4		ipoglb.g	⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐼 ) )
5		ipoglbdm.t	⊢ ( 𝜑 → 𝑇 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } )
6	1	ipobas	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 = ( Base ‘ 𝐼 ) )
7	2 6	syl	⊢ ( 𝜑 → 𝐹 = ( Base ‘ 𝐼 ) )
8		eqidd	⊢ ( 𝜑 → ( le ‘ 𝐼 ) = ( le ‘ 𝐼 ) )
9		eqid	⊢ ( le ‘ 𝐼 ) = ( le ‘ 𝐼 )
10	1 2 3 9	ipoglblem	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ) → ( ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑦 ∧ ∀ 𝑧 ∈ 𝐹 ( ∀ 𝑦 ∈ 𝑆 𝑧 ( le ‘ 𝐼 ) 𝑦 → 𝑧 ( le ‘ 𝐼 ) 𝑤 ) ) ) )
11	1	ipopos	⊢ 𝐼 ∈ Poset
12	11	a1i	⊢ ( 𝜑 → 𝐼 ∈ Poset )
13	7 8 4 10 12	glbeldm2d	⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐹 ∧ ∃ 𝑤 ∈ 𝐹 ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ) ) )
14	3 13	mpbirand	⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ∃ 𝑤 ∈ 𝐹 ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ) )
15	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ) ∧ ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ) → 𝑇 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } )
16		unilbeu	⊢ ( 𝑤 ∈ 𝐹 → ( ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ↔ 𝑤 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } ) )
17	16	biimpa	⊢ ( ( 𝑤 ∈ 𝐹 ∧ ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ) → 𝑤 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } )
18	17	adantll	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ) ∧ ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ) → 𝑤 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } )
19	15 18	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ) ∧ ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ) → 𝑇 = 𝑤 )
20		simplr	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ) ∧ ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ) → 𝑤 ∈ 𝐹 )
21	19 20	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ) ∧ ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ) → 𝑇 ∈ 𝐹 )
22	21	ex	⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐹 ) → ( ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) → 𝑇 ∈ 𝐹 ) )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑇 ∈ 𝐹 ) → 𝑇 ∈ 𝐹 )
24		unilbeu	⊢ ( 𝑇 ∈ 𝐹 → ( ( 𝑇 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) ↔ 𝑇 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } ) )
25	24	biimparc	⊢ ( ( 𝑇 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ 𝑆 } ∧ 𝑇 ∈ 𝐹 ) → ( 𝑇 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) )
26	5 25	sylan	⊢ ( ( 𝜑 ∧ 𝑇 ∈ 𝐹 ) → ( 𝑇 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) )
27		sseq1	⊢ ( 𝑤 = 𝑇 → ( 𝑤 ⊆ ∩ 𝑆 ↔ 𝑇 ⊆ ∩ 𝑆 ) )
28		sseq2	⊢ ( 𝑤 = 𝑇 → ( 𝑧 ⊆ 𝑤 ↔ 𝑧 ⊆ 𝑇 ) )
29	28	imbi2d	⊢ ( 𝑤 = 𝑇 → ( ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ↔ ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) )
30	29	ralbidv	⊢ ( 𝑤 = 𝑇 → ( ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ↔ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) )
31	27 30	anbi12d	⊢ ( 𝑤 = 𝑇 → ( ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ↔ ( 𝑇 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑇 ) ) ) )
32	22 23 26 31	rspceb2dv	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ 𝐹 ( 𝑤 ⊆ ∩ 𝑆 ∧ ∀ 𝑧 ∈ 𝐹 ( 𝑧 ⊆ ∩ 𝑆 → 𝑧 ⊆ 𝑤 ) ) ↔ 𝑇 ∈ 𝐹 ) )
33	14 32	bitrd	⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ 𝑇 ∈ 𝐹 ) )