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 = ( toInc ` F )
	ipolub0.u	|- ( ph -> U = ( lub ` I ) )
	ipolub0.f	|- ( ph -> |^| F e. F )
	ipolub0.v	|- ( ph -> F e. V )
Assertion	ipolub0	|- ( ph -> ( U ` (/) ) = |^| F )

Proof

Step	Hyp	Ref	Expression
1		ipoglb0.i	|- I = ( toInc ` F )
2		ipolub0.u	|- ( ph -> U = ( lub ` I ) )
3		ipolub0.f	|- ( ph -> |^| F e. F )
4		ipolub0.v	|- ( ph -> F e. V )
5		0ss	|- (/) C_ F
6	5	a1i	|- ( ph -> (/) C_ F )
7		uni0	|- U. (/) = (/)
8		0ss	|- (/) C_ x
9	7 8	eqsstri	|- U. (/) C_ x
10	9	a1i	|- ( x e. F -> U. (/) C_ x )
11	10	rabeqc	|- { x e. F | U. (/) C_ x } = F
12	11	eqcomi	|- F = { x e. F | U. (/) C_ x }
13	12	inteqi	|- |^| F = |^| { x e. F | U. (/) C_ x }
14	13	a1i	|- ( ph -> |^| F = |^| { x e. F | U. (/) C_ x } )
15	1 4 6 2 14 3	ipolub	|- ( ph -> ( U ` (/) ) = |^| F )