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 = ( toInc ` F )
	ipoglb0.g	|- ( ph -> G = ( glb ` I ) )
	ipoglb0.f	|- ( ph -> U. F e. F )
Assertion	ipoglb0	|- ( ph -> ( G ` (/) ) = U. F )

Proof

Step	Hyp	Ref	Expression
1		ipoglb0.i	|- I = ( toInc ` F )
2		ipoglb0.g	|- ( ph -> G = ( glb ` I ) )
3		ipoglb0.f	|- ( ph -> U. F e. F )
4		uniexr	|- ( U. F e. F -> F e. _V )
5	3 4	syl	|- ( ph -> F e. _V )
6		0ss	|- (/) C_ F
7	6	a1i	|- ( ph -> (/) C_ F )
8		ssv	|- x C_ _V
9		int0	|- |^| (/) = _V
10	8 9	sseqtrri	|- x C_ |^| (/)
11	10	a1i	|- ( x e. F -> x C_ |^| (/) )
12	11	rabeqc	|- { x e. F | x C_ |^| (/) } = F
13	12	unieqi	|- U. { x e. F | x C_ |^| (/) } = U. F
14	13	eqcomi	|- U. F = U. { x e. F | x C_ |^| (/) }
15	14	a1i	|- ( ph -> U. F = U. { x e. F | x C_ |^| (/) } )
16	1 5 7 2 15 3	ipoglb	|- ( ph -> ( G ` (/) ) = U. F )