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 biimpri 
 |-  ( A. y e. B ( A C_ y -> C C_ y ) -> C C_ |^| { x e. B | A C_ x } )
6 5 adantl 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> C C_ |^| { x e. B | A C_ x } )
7 sseq2 
 |-  ( z = C -> ( A C_ z <-> A C_ C ) )
8 simpll 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> C e. B )
9 simplr 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> A C_ C )
10 7 8 9 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 } )
11 sseq2 
 |-  ( z = x -> ( A C_ z <-> A C_ x ) )
12 11 cbvrabv 
 |-  { z e. B | A C_ z } = { x e. B | A C_ x }
13 10 12 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 } )
14 intss1 
 |-  ( C e. { x e. B | A C_ x } -> |^| { x e. B | A C_ x } C_ C )
15 13 14 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 )
16 6 15 eqssd 
 |-  ( ( ( C e. B /\ A C_ C ) /\ A. y e. B ( A C_ y -> C C_ y ) ) -> C = |^| { x e. B | A C_ x } )
17 16 expl 
 |-  ( C e. B -> ( ( A C_ C /\ A. y e. B ( A C_ y -> C C_ y ) ) -> C = |^| { x e. B | A C_ x } ) )
18 ssintub 
 |-  A C_ |^| { x e. B | A C_ x }
19 sseq2 
 |-  ( C = |^| { x e. B | A C_ x } -> ( A C_ C <-> A C_ |^| { x e. B | A C_ x } ) )
20 18 19 mpbiri 
 |-  ( C = |^| { x e. B | A C_ x } -> A C_ C )
21 eqimss 
 |-  ( C = |^| { x e. B | A C_ x } -> C C_ |^| { x e. B | A C_ x } )
22 21 4 sylib 
 |-  ( C = |^| { x e. B | A C_ x } -> A. y e. B ( A C_ y -> C C_ y ) )
23 20 22 jca 
 |-  ( C = |^| { x e. B | A C_ x } -> ( A C_ C /\ A. y e. B ( A C_ y -> C C_ y ) ) )
24 17 23 impbid1 
 |-  ( C e. B -> ( ( A C_ C /\ A. y e. B ( A C_ y -> C C_ y ) ) <-> C = |^| { x e. B | A C_ x } ) )