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 bilanri 
 |-  ( ( ( 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 )
15 9 14 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 } )
16 15 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 } ) )
17 unilbss 
 |-  U. { x e. B | x C_ A } C_ A
18 sseq1 
 |-  ( C = U. { x e. B | x C_ A } -> ( C C_ A <-> U. { x e. B | x C_ A } C_ A ) )
19 17 18 mpbiri 
 |-  ( C = U. { x e. B | x C_ A } -> C C_ A )
20 eqimss2 
 |-  ( C = U. { x e. B | x C_ A } -> U. { x e. B | x C_ A } C_ C )
21 20 13 sylib 
 |-  ( C = U. { x e. B | x C_ A } -> A. y e. B ( y C_ A -> y C_ C ) )
22 19 21 jca 
 |-  ( C = U. { x e. B | x C_ A } -> ( C C_ A /\ A. y e. B ( y C_ A -> y C_ C ) ) )
23 16 22 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 } ) )