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	⊢ 𝐼 = ( toInc ‘ 𝐹 )
	ipoglb0.g	⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐼 ) )
	ipoglb0.f	⊢ ( 𝜑 → ∪ 𝐹 ∈ 𝐹 )
Assertion	ipoglb0	⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = ∪ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		ipoglb0.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
2		ipoglb0.g	⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐼 ) )
3		ipoglb0.f	⊢ ( 𝜑 → ∪ 𝐹 ∈ 𝐹 )
4		uniexr	⊢ ( ∪ 𝐹 ∈ 𝐹 → 𝐹 ∈ V )
5	3 4	syl	⊢ ( 𝜑 → 𝐹 ∈ V )
6		0ss	⊢ ∅ ⊆ 𝐹
7	6	a1i	⊢ ( 𝜑 → ∅ ⊆ 𝐹 )
8		ssv	⊢ 𝑥 ⊆ V
9		int0	⊢ ∩ ∅ = V
10	8 9	sseqtrri	⊢ 𝑥 ⊆ ∩ ∅
11	10	a1i	⊢ ( 𝑥 ∈ 𝐹 → 𝑥 ⊆ ∩ ∅ )
12	11	rabeqc	⊢ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ ∅ } = 𝐹
13	12	unieqi	⊢ ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ ∅ } = ∪ 𝐹
14	13	eqcomi	⊢ ∪ 𝐹 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ ∅ }
15	14	a1i	⊢ ( 𝜑 → ∪ 𝐹 = ∪ { 𝑥 ∈ 𝐹 ∣ 𝑥 ⊆ ∩ ∅ } )
16	1 5 7 2 15 3	ipoglb	⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = ∪ 𝐹 )