Theorem ipoglb0

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

	Ref	Expression
Hypotheses	ipoglb0.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
	ipoglb0.g	$$⊢\phi \to G=\mathrm{glb}\left(I\right)$$
	ipoglb0.f	$$⊢\phi \to \bigcup F\in F$$
Assertion	ipoglb0	$$⊢\phi \to G\left(\varnothing \right)=\bigcup F$$

Proof

Step	Hyp	Ref	Expression
1		ipoglb0.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
2		ipoglb0.g	$$⊢\phi \to G=\mathrm{glb}\left(I\right)$$
3		ipoglb0.f	$$⊢\phi \to \bigcup F\in F$$
4		uniexr	$$⊢\bigcup F\in F\to F\in \mathrm{V}$$
5	3 4	syl	$$⊢\phi \to F\in \mathrm{V}$$
6		0ss	$$⊢\varnothing \subseteq F$$
7	6	a1i	$$⊢\phi \to \varnothing \subseteq F$$
8		ssv	$$⊢x\subseteq \mathrm{V}$$
9		int0	$$⊢\bigcap \varnothing =\mathrm{V}$$
10	8 9	sseqtrri	$$⊢x\subseteq \bigcap \varnothing$$
11	10	a1i	$$⊢x\in F\to x\subseteq \bigcap \varnothing$$
12	11	rabeqc	$$⊢\left\{x\in F|x\subseteq \bigcap \varnothing \right\}=F$$
13	12	unieqi	$$⊢\bigcup \left\{x\in F|x\subseteq \bigcap \varnothing \right\}=\bigcup F$$
14	13	eqcomi	$$⊢\bigcup F=\bigcup \left\{x\in F|x\subseteq \bigcap \varnothing \right\}$$
15	14	a1i	$$⊢\phi \to \bigcup F=\bigcup \left\{x\in F|x\subseteq \bigcap \varnothing \right\}$$
16	1 5 7 2 15 3	ipoglb	$$⊢\phi \to G\left(\varnothing \right)=\bigcup F$$