ipoglbdm

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

	Ref	Expression
Hypotheses	ipolub.i	$⊢ I = toInc (F)$
	ipolub.f	$⊢ φ \to F \in V$
	ipolub.s	$⊢ φ \to S \subseteq F$
	ipoglb.g	$⊢ φ \to G = glb (I)$
	ipoglbdm.t	$⊢ φ \to T = ⋃ \{x \in F \| x \subseteq ⋂ S\}$
Assertion	ipoglbdm	$⊢ φ \to (S \in dom G \leftrightarrow T \in F)$

Proof

Step	Hyp	Ref	Expression
1		ipolub.i	$⊢ I = toInc (F)$
2		ipolub.f	$⊢ φ \to F \in V$
3		ipolub.s	$⊢ φ \to S \subseteq F$
4		ipoglb.g	$⊢ φ \to G = glb (I)$
5		ipoglbdm.t	$⊢ φ \to T = ⋃ \{x \in F \| x \subseteq ⋂ S\}$
6	1	ipobas	$⊢ F \in V \to F = {Base}_{I}$
7	2 6	syl	$⊢ φ \to F = {Base}_{I}$
8		eqidd	$⊢ φ \to \leq_{I} = \leq_{I}$
9		eqid	$⊢ \leq_{I} = \leq_{I}$
10	1 2 3 9	ipoglblem	$⊢ (φ \land w \in F) \to ((w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w)) \leftrightarrow (\forall y \in S w \leq_{I} y \land \forall z \in F (\forall y \in S z \leq_{I} y \to z \leq_{I} w)))$
11	1	ipopos	$⊢ I \in Poset$
12	11	a1i	$⊢ φ \to I \in Poset$
13	7 8 4 10 12	glbeldm2d	$⊢ φ \to (S \in dom G \leftrightarrow (S \subseteq F \land \exists w \in F (w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w))))$
14	3 13	mpbirand	$⊢ φ \to (S \in dom G \leftrightarrow \exists w \in F (w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w)))$
15	5	ad2antrr	$⊢ ((φ \land w \in F) \land (w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w))) \to T = ⋃ \{x \in F \| x \subseteq ⋂ S\}$
16		unilbeu	$⊢ w \in F \to ((w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w)) \leftrightarrow w = ⋃ \{x \in F \| x \subseteq ⋂ S\})$
17	16	biimpa	$⊢ (w \in F \land (w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w))) \to w = ⋃ \{x \in F \| x \subseteq ⋂ S\}$
18	17	adantll	$⊢ ((φ \land w \in F) \land (w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w))) \to w = ⋃ \{x \in F \| x \subseteq ⋂ S\}$
19	15 18	eqtr4d	$⊢ ((φ \land w \in F) \land (w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w))) \to T = w$
20		simplr	$⊢ ((φ \land w \in F) \land (w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w))) \to w \in F$
21	19 20	eqeltrd	$⊢ ((φ \land w \in F) \land (w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w))) \to T \in F$
22	21	ex	$⊢ (φ \land w \in F) \to ((w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w)) \to T \in F)$
23		simpr	$⊢ (φ \land T \in F) \to T \in F$
24		unilbeu	$⊢ T \in F \to ((T \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq T)) \leftrightarrow T = ⋃ \{x \in F \| x \subseteq ⋂ S\})$
25	24	biimparc	$⊢ (T = ⋃ \{x \in F \| x \subseteq ⋂ S\} \land T \in F) \to (T \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq T))$
26	5 25	sylan	$⊢ (φ \land T \in F) \to (T \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq T))$
27		sseq1	$⊢ w = T \to (w \subseteq ⋂ S \leftrightarrow T \subseteq ⋂ S)$
28		sseq2	$⊢ w = T \to (z \subseteq w \leftrightarrow z \subseteq T)$
29	28	imbi2d	$⊢ w = T \to ((z \subseteq ⋂ S \to z \subseteq w) \leftrightarrow (z \subseteq ⋂ S \to z \subseteq T))$
30	29	ralbidv	$⊢ w = T \to (\forall z \in F (z \subseteq ⋂ S \to z \subseteq w) \leftrightarrow \forall z \in F (z \subseteq ⋂ S \to z \subseteq T))$
31	27 30	anbi12d	$⊢ w = T \to ((w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w)) \leftrightarrow (T \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq T)))$
32	22 23 26 31	rspceb2dv	$⊢ φ \to (\exists w \in F (w \subseteq ⋂ S \land \forall z \in F (z \subseteq ⋂ S \to z \subseteq w)) \leftrightarrow T \in F)$
33	14 32	bitrd	$⊢ φ \to (S \in dom G \leftrightarrow T \in F)$

Metamath Proof Explorer

Theorem ipoglbdm

Proof