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

Metamath Proof Explorer

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 ⊢ φ → U = lub ⁡ I
ipolub0.f ⊢ φ → ⋂ F ∈ F
ipolub0.v ⊢ φ → F ∈ V
Assertion ipolub0 ⊢ φ → U ⁡ ∅ = ⋂ F

Proof

Step Hyp Ref Expression
1 ipoglb0.i ⊢ I = toInc ⁡ F
2 ipolub0.u ⊢ φ → U = lub ⁡ I
3 ipolub0.f ⊢ φ → ⋂ F ∈ F
4 ipolub0.v ⊢ φ → F ∈ V
5 0ss ⊢ ∅ ⊆ F
6 5 a1i ⊢ φ → ∅ ⊆ F
7 uni0 ⊢ ⋃ ∅ = ∅
8 0ss ⊢ ∅ ⊆ x
9 7 8 eqsstri ⊢ ⋃ ∅ ⊆ x
10 9 a1i ⊢ x ∈ F → ⋃ ∅ ⊆ x
11 10 rabeqc ⊢ x ∈ F | ⋃ ∅ ⊆ x = F
12 11 eqcomi ⊢ F = x ∈ F | ⋃ ∅ ⊆ x
13 12 inteqi ⊢ ⋂ F = ⋂ x ∈ F | ⋃ ∅ ⊆ x
14 13 a1i ⊢ φ → ⋂ F = ⋂ x ∈ F | ⋃ ∅ ⊆ x
15 1 4 6 2 14 3 ipolub ⊢ φ → U ⁡ ∅ = ⋂ F