This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = ∪ 𝐹 )