Theorem ipolub0

Description: The LUB of the empty set is the intersection of the base. (Contributed by Zhi Wang, 30-Sep-2024)

	Ref	Expression
Hypotheses	ipoglb0.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
	ipolub0.u	$$⊢\phi \to U=\mathrm{lub}\left(I\right)$$
	ipolub0.f	$$⊢\phi \to \bigcap F\in F$$
	ipolub0.v	$$⊢\phi \to F\in V$$
Assertion	ipolub0	$$⊢\phi \to U\left(\varnothing \right)=\bigcap F$$

Proof

Step	Hyp	Ref	Expression
1		ipoglb0.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
2		ipolub0.u	$$⊢\phi \to U=\mathrm{lub}\left(I\right)$$
3		ipolub0.f	$$⊢\phi \to \bigcap F\in F$$
4		ipolub0.v	$$⊢\phi \to F\in V$$
5		0ss	$$⊢\varnothing \subseteq F$$
6	5	a1i	$$⊢\phi \to \varnothing \subseteq F$$
7		uni0	$$⊢\bigcup \varnothing =\varnothing$$
8		0ss	$$⊢\varnothing \subseteq x$$
9	7 8	eqsstri	$$⊢\bigcup \varnothing \subseteq x$$
10	9	a1i	$$⊢x\in F\to \bigcup \varnothing \subseteq x$$
11	10	rabeqc	$$⊢\left\{x\in F|\bigcup \varnothing \subseteq x\right\}=F$$
12	11	eqcomi	$$⊢F=\left\{x\in F|\bigcup \varnothing \subseteq x\right\}$$
13	12	inteqi	$$⊢\bigcap F=\bigcap \left\{x\in F|\bigcup \varnothing \subseteq x\right\}$$
14	13	a1i	$$⊢\phi \to \bigcap F=\bigcap \left\{x\in F|\bigcup \varnothing \subseteq x\right\}$$
15	1 4 6 2 14 3	ipolub	$$⊢\phi \to U\left(\varnothing \right)=\bigcap F$$