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	⊢ 𝐼 = ( toInc ‘ 𝐹 )
	ipolub0.u	⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐼 ) )
	ipolub0.f	⊢ ( 𝜑 → ∩ 𝐹 ∈ 𝐹 )
	ipolub0.v	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
Assertion	ipolub0	⊢ ( 𝜑 → ( 𝑈 ‘ ∅ ) = ∩ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		ipoglb0.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
2		ipolub0.u	⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐼 ) )
3		ipolub0.f	⊢ ( 𝜑 → ∩ 𝐹 ∈ 𝐹 )
4		ipolub0.v	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
5		0ss	⊢ ∅ ⊆ 𝐹
6	5	a1i	⊢ ( 𝜑 → ∅ ⊆ 𝐹 )
7		uni0	⊢ ∪ ∅ = ∅
8		0ss	⊢ ∅ ⊆ 𝑥
9	7 8	eqsstri	⊢ ∪ ∅ ⊆ 𝑥
10	9	a1i	⊢ ( 𝑥 ∈ 𝐹 → ∪ ∅ ⊆ 𝑥 )
11	10	rabeqc	⊢ { 𝑥 ∈ 𝐹 ∣ ∪ ∅ ⊆ 𝑥 } = 𝐹
12	11	eqcomi	⊢ 𝐹 = { 𝑥 ∈ 𝐹 ∣ ∪ ∅ ⊆ 𝑥 }
13	12	inteqi	⊢ ∩ 𝐹 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ ∅ ⊆ 𝑥 }
14	13	a1i	⊢ ( 𝜑 → ∩ 𝐹 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ ∅ ⊆ 𝑥 } )
15	1 4 6 2 14 3	ipolub	⊢ ( 𝜑 → ( 𝑈 ‘ ∅ ) = ∩ 𝐹 )