Metamath Proof Explorer

Theorem unilbeu

Description: Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Assertion unilbeu 
|- ( C e. B -> ( ( C C_ A /\ A. y e. B ( y C_ A -> y C_ C ) ) <-> C = U. { x e. B | x C_ A } ) )

Proof

Step Hyp Ref Expression
1 sseq1 
 |-  ( z = C -> ( z C_ A <-> C C_ A ) )
2 simpll 
 |-  ( ( ( C e. B /\ C C_ A ) /\ A. y e. B ( y C_ A -> y C_ C ) ) -> C e. B )
3 simplr 
 |-  ( ( ( C e. B /\ C C_ A ) /\ A. y e. B ( y C_ A -> y C_ C ) ) -> C C_ A )
4 1 2 3 elrabd 
 |-  ( ( ( C e. B /\ C C_ A ) /\ A. y e. B ( y C_ A -> y C_ C ) ) -> C e. { z e. B | z C_ A } )
5 sseq1 
 |-  ( z = x -> ( z C_ A <-> x C_ A ) )
6 5 cbvrabv 
 |-  { z e. B | z C_ A } = { x e. B | x C_ A }
7 4 6 eleqtrdi 
 |-  ( ( ( C e. B /\ C C_ A ) /\ A. y e. B ( y C_ A -> y C_ C ) ) -> C e. { x e. B | x C_ A } )
8 elssuni 
 |-  ( C e. { x e. B | x C_ A } -> C C_ U. { x e. B | x C_ A } )
9 7 8 syl 
 |-  ( ( ( C e. B /\ C C_ A ) /\ A. y e. B ( y C_ A -> y C_ C ) ) -> C C_ U. { x e. B | x C_ A } )
10 unissb 
 |-  ( U. { x e. B | x C_ A } C_ C <-> A. y e. { x e. B | x C_ A } y C_ C )
11 sseq1 
 |-  ( x = y -> ( x C_ A <-> y C_ A ) )
12 11 ralrab 
 |-  ( A. y e. { x e. B | x C_ A } y C_ C <-> A. y e. B ( y C_ A -> y C_ C ) )
13 10 12 bitri 
 |-  ( U. { x e. B | x C_ A } C_ C <-> A. y e. B ( y C_ A -> y C_ C ) )
14 13 biimpri 
 |-  ( A. y e. B ( y C_ A -> y C_ C ) -> U. { x e. B | x C_ A } C_ C )
15 14 adantl 
 |-  ( ( ( C e. B /\ C C_ A ) /\ A. y e. B ( y C_ A -> y C_ C ) ) -> U. { x e. B | x C_ A } C_ C )
16 9 15 eqssd 
 |-  ( ( ( C e. B /\ C C_ A ) /\ A. y e. B ( y C_ A -> y C_ C ) ) -> C = U. { x e. B | x C_ A } )
17 16 expl 
 |-  ( C e. B -> ( ( C C_ A /\ A. y e. B ( y C_ A -> y C_ C ) ) -> C = U. { x e. B | x C_ A } ) )
18 unilbss 
 |-  U. { x e. B | x C_ A } C_ A
19 sseq1 
 |-  ( C = U. { x e. B | x C_ A } -> ( C C_ A <-> U. { x e. B | x C_ A } C_ A ) )
20 18 19 mpbiri 
 |-  ( C = U. { x e. B | x C_ A } -> C C_ A )
21 eqimss2 
 |-  ( C = U. { x e. B | x C_ A } -> U. { x e. B | x C_ A } C_ C )
22 21 13 sylib 
 |-  ( C = U. { x e. B | x C_ A } -> A. y e. B ( y C_ A -> y C_ C ) )
23 20 22 jca 
 |-  ( C = U. { x e. B | x C_ A } -> ( C C_ A /\ A. y e. B ( y C_ A -> y C_ C ) ) )
24 17 23 impbid1 
 |-  ( C e. B -> ( ( C C_ A /\ A. y e. B ( y C_ A -> y C_ C ) ) <-> C = U. { x e. B | x C_ A } ) )