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

Metamath Proof Explorer

Theorem unilbss

Description: Superclass of the greatest lower bound. A dual statement of ssintub . (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Assertion unilbss ⊢ ⋃ x ∈ B | x ⊆ A ⊆ A

Proof

Step Hyp Ref Expression
1 unissb ⊢ ⋃ x ∈ B | x ⊆ A ⊆ A ↔ ∀ y ∈ x ∈ B | x ⊆ A y ⊆ A
2 sseq1 ⊢ x = y → x ⊆ A ↔ y ⊆ A
3 2 elrab ⊢ y ∈ x ∈ B | x ⊆ A ↔ y ∈ B ∧ y ⊆ A
4 3 simprbi ⊢ y ∈ x ∈ B | x ⊆ A → y ⊆ A
5 1 4 mprgbir ⊢ ⋃ x ∈ B | x ⊆ A ⊆ A