Metamath Proof Explorer

Theorem intubeu

Description: Existential uniqueness of the least upper bound. (Contributed by Zhi Wang, 28-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 ssint 
 |-  ( C C_ |^| { x e. B | A C_ x } <-> A. y e. { x e. B | A C_ x } C C_ y )
2 sseq2 
 |-  ( x = y -> ( A C_ x <-> A C_ y ) )
3 2 ralrab 
 |-  ( A. y e. { x e. B | A C_ x } C C_ y <-> A. y e. B ( A C_ y -> C C_ y ) )
4 1 3 bitri 
 |-  ( C C_ |^| { x e. B | A C_ x } <-> A. y e. B ( A C_ y -> C C_ y ) )
5 4 bilanri 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> C C_ |^| { x e. B | A C_ x } )
6 sseq2 
 |-  ( z = C -> ( A C_ z <-> A C_ C ) )
7 simpll 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> C e. B )
8 simplr 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> A C_ C )
9 6 7 8 elrabd 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> C e. { z e. B | A C_ z } )
10 sseq2 
 |-  ( z = x -> ( A C_ z <-> A C_ x ) )
11 10 cbvrabv 
 |-  { z e. B | A C_ z } = { x e. B | A C_ x }
12 9 11 eleqtrdi 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> C e. { x e. B | A C_ x } )
13 intss1 
 |-  ( C e. { x e. B | A C_ x } -> |^| { x e. B | A C_ x } C_ C )
14 12 13 syl 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> |^| { x e. B | A C_ x } C_ C )
15 5 14 eqssd 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> C = |^| { x e. B | A C_ x } )
16 15 expl 
 |-  ( C e. B -> ( ( A C_ C /\ A. y e. B ( A C_ y -> C C_ y ) ) -> C = |^| { x e. B | A C_ x } ) )
17 ssintub 
 |-  A C_ |^| { x e. B | A C_ x }
18 sseq2 
 |-  ( C = |^| { x e. B | A C_ x } -> ( A C_ C <-> A C_ |^| { x e. B | A C_ x } ) )
19 17 18 mpbiri 
 |-  ( C = |^| { x e. B | A C_ x } -> A C_ C )
20 eqimss 
 |-  ( C = |^| { x e. B | A C_ x } -> C C_ |^| { x e. B | A C_ x } )
21 20 4 sylib 
 |-  ( C = |^| { x e. B | A C_ x } -> A. y e. B ( A C_ y -> C C_ y ) )
22 19 21 jca 
 |-  ( C = |^| { x e. B | A C_ x } -> ( A C_ C /\ A. y e. B ( A C_ y -> C C_ y ) ) )
23 16 22 impbid1 
 |-  ( C e. B -> ( ( A C_ C /\ A. y e. B ( A C_ y -> C C_ y ) ) <-> C = |^| { x e. B | A C_ x } ) )