Metamath Proof Explorer

Theorem eqsup

Description: Sufficient condition for an element to be equal to the supremum. (Contributed by Mario Carneiro, 21-Apr-2015)

Ref Expression
Hypothesis supmo.1 
|- ( ph -> R Or A )
Assertion eqsup 
|- ( ph -> ( ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) -> sup ( B , A , R ) = C ) )

Proof

Step Hyp Ref Expression
1 supmo.1 
 |-  ( ph -> R Or A )
2 1 adantr 
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) -> R Or A )
3 2 supval2 
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) -> sup ( B , A , R ) = ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
4 3simpc 
 |-  ( ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) -> ( A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) )
5 4 adantl 
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) -> ( A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) )
6 simpr1 
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) -> C e. A )
7 breq1 
 |-  ( x = C -> ( x R y <-> C R y ) )
8 7 notbid 
 |-  ( x = C -> ( -. x R y <-> -. C R y ) )
9 8 ralbidv 
 |-  ( x = C -> ( A. y e. B -. x R y <-> A. y e. B -. C R y ) )
10 breq2 
 |-  ( x = C -> ( y R x <-> y R C ) )
11 10 imbi1d 
 |-  ( x = C -> ( ( y R x -> E. z e. B y R z ) <-> ( y R C -> E. z e. B y R z ) ) )
12 11 ralbidv 
 |-  ( x = C -> ( A. y e. A ( y R x -> E. z e. B y R z ) <-> A. y e. A ( y R C -> E. z e. B y R z ) ) )
13 9 12 anbi12d 
 |-  ( x = C -> ( ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) <-> ( A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) )
14 13 rspcev 
 |-  ( ( C e. A /\ ( A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
15 6 5 14 syl2anc 
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
16 2 15 supeu 
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) -> E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
17 13 riota2 
 |-  ( ( C e. A /\ E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) -> ( ( A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) <-> ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) = C ) )
18 6 16 17 syl2anc 
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) -> ( ( A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) <-> ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) = C ) )
19 5 18 mpbid 
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) -> ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) = C )
20 3 19 eqtrd 
 |-  ( ( ph /\ ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) ) -> sup ( B , A , R ) = C )
21 20 ex 
 |-  ( ph -> ( ( C e. A /\ A. y e. B -. C R y /\ A. y e. A ( y R C -> E. z e. B y R z ) ) -> sup ( B , A , R ) = C ) )