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 
|- U. { x e. B | x C_ A } C_ A

Proof

Step Hyp Ref Expression
1 unissb 
 |-  ( U. { x e. B | x C_ A } C_ A <-> A. y e. { x e. B | x C_ A } y C_ A )
2 sseq1 
 |-  ( x = y -> ( x C_ A <-> y C_ A ) )
3 2 elrab 
 |-  ( y e. { x e. B | x C_ A } <-> ( y e. B /\ y C_ A ) )
4 3 simprbi 
 |-  ( y e. { x e. B | x C_ A } -> y C_ A )
5 1 4 mprgbir 
 |-  U. { x e. B | x C_ A } C_ A