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 ⊢ I = toInc ⁡ F
ipoglb0.g ⊢ φ → G = glb ⁡ I
ipoglb0.f ⊢ φ → ⋃ F ∈ F
Assertion ipoglb0 ⊢ φ → G ⁡ ∅ = ⋃ F

Proof

Step Hyp Ref Expression
1 ipoglb0.i ⊢ I = toInc ⁡ F
2 ipoglb0.g ⊢ φ → G = glb ⁡ I
3 ipoglb0.f ⊢ φ → ⋃ F ∈ F
4 uniexr ⊢ ⋃ F ∈ F → F ∈ V
5 3 4 syl ⊢ φ → F ∈ V
6 0ss ⊢ ∅ ⊆ F
7 6 a1i ⊢ φ → ∅ ⊆ F
8 ssv ⊢ x ⊆ V
9 int0 ⊢ ⋂ ∅ = V
10 8 9 sseqtrri ⊢ x ⊆ ⋂ ∅
11 10 a1i ⊢ x ∈ F → x ⊆ ⋂ ∅
12 11 rabeqc ⊢ x ∈ F | x ⊆ ⋂ ∅ = F
13 12 unieqi ⊢ ⋃ x ∈ F | x ⊆ ⋂ ∅ = ⋃ F
14 13 eqcomi ⊢ ⋃ F = ⋃ x ∈ F | x ⊆ ⋂ ∅
15 14 a1i ⊢ φ → ⋃ F = ⋃ x ∈ F | x ⊆ ⋂ ∅
16 1 5 7 2 15 3 ipoglb ⊢ φ → G ⁡ ∅ = ⋃ F