ipolubdm

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

	Ref	Expression
Hypotheses	ipolub.i	$⊢ I = toInc (F)$
	ipolub.f	$⊢ φ \to F \in V$
	ipolub.s	$⊢ φ \to S \subseteq F$
	ipolub.u	$⊢ φ \to U = lub (I)$
	ipolubdm.t	$⊢ φ \to T = ⋂ \{x \in F \| ⋃ S \subseteq x\}$
Assertion	ipolubdm	$⊢ φ \to (S \in dom U \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		ipolub.u	$⊢ φ \to U = lub (I)$
5		ipolubdm.t	$⊢ φ \to T = ⋂ \{x \in F \| ⋃ S \subseteq x\}$
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	ipolublem	$⊢ (φ \land t \in F) \to ((⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z)) \leftrightarrow (\forall y \in S y \leq_{I} t \land \forall z \in F (\forall y \in S y \leq_{I} z \to t \leq_{I} z)))$
11	1	ipopos	$⊢ I \in Poset$
12	11	a1i	$⊢ φ \to I \in Poset$
13	7 8 4 10 12	lubeldm2d	$⊢ φ \to (S \in dom U \leftrightarrow (S \subseteq F \land \exists t \in F (⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z))))$
14	3 13	mpbirand	$⊢ φ \to (S \in dom U \leftrightarrow \exists t \in F (⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z)))$
15	5	ad2antrr	$⊢ ((φ \land t \in F) \land (⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z))) \to T = ⋂ \{x \in F \| ⋃ S \subseteq x\}$
16		intubeu	$⊢ t \in F \to ((⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z)) \leftrightarrow t = ⋂ \{x \in F \| ⋃ S \subseteq x\})$
17	16	biimpa	$⊢ (t \in F \land (⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z))) \to t = ⋂ \{x \in F \| ⋃ S \subseteq x\}$
18	17	adantll	$⊢ ((φ \land t \in F) \land (⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z))) \to t = ⋂ \{x \in F \| ⋃ S \subseteq x\}$
19	15 18	eqtr4d	$⊢ ((φ \land t \in F) \land (⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z))) \to T = t$
20		simplr	$⊢ ((φ \land t \in F) \land (⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z))) \to t \in F$
21	19 20	eqeltrd	$⊢ ((φ \land t \in F) \land (⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z))) \to T \in F$
22	21	ex	$⊢ (φ \land t \in F) \to ((⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z)) \to T \in F)$
23		simpr	$⊢ (φ \land T \in F) \to T \in F$
24		intubeu	$⊢ T \in F \to ((⋃ S \subseteq T \land \forall z \in F (⋃ S \subseteq z \to T \subseteq z)) \leftrightarrow T = ⋂ \{x \in F \| ⋃ S \subseteq x\})$
25	24	biimparc	$⊢ (T = ⋂ \{x \in F \| ⋃ S \subseteq x\} \land T \in F) \to (⋃ S \subseteq T \land \forall z \in F (⋃ S \subseteq z \to T \subseteq z))$
26	5 25	sylan	$⊢ (φ \land T \in F) \to (⋃ S \subseteq T \land \forall z \in F (⋃ S \subseteq z \to T \subseteq z))$
27		sseq2	$⊢ t = T \to (⋃ S \subseteq t \leftrightarrow ⋃ S \subseteq T)$
28		sseq1	$⊢ t = T \to (t \subseteq z \leftrightarrow T \subseteq z)$
29	28	imbi2d	$⊢ t = T \to ((⋃ S \subseteq z \to t \subseteq z) \leftrightarrow (⋃ S \subseteq z \to T \subseteq z))$
30	29	ralbidv	$⊢ t = T \to (\forall z \in F (⋃ S \subseteq z \to t \subseteq z) \leftrightarrow \forall z \in F (⋃ S \subseteq z \to T \subseteq z))$
31	27 30	anbi12d	$⊢ t = T \to ((⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z)) \leftrightarrow (⋃ S \subseteq T \land \forall z \in F (⋃ S \subseteq z \to T \subseteq z)))$
32	22 23 26 31	rspceb2dv	$⊢ φ \to (\exists t \in F (⋃ S \subseteq t \land \forall z \in F (⋃ S \subseteq z \to t \subseteq z)) \leftrightarrow T \in F)$
33	14 32	bitrd	$⊢ φ \to (S \in dom U \leftrightarrow T \in F)$

Metamath Proof Explorer

Theorem ipolubdm

Proof