This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suplub2

Description: Bidirectional form of suplub . (Contributed by Mario Carneiro, 6-Sep-2014)

Ref Expression
Hypotheses supmo.1 
|- ( ph -> R Or A )
supcl.2 
|- ( ph -> 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 ) ) )
suplub2.3 
|- ( ph -> B C_ A )
Assertion suplub2 
|- ( ( ph /\ C e. A ) -> ( C R sup ( B , A , R ) <-> E. z e. B C R z ) )

Proof

Step Hyp Ref Expression
1 supmo.1 
 |-  ( ph -> R Or A )
2 supcl.2 
 |-  ( ph -> 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 ) ) )
3 suplub2.3 
 |-  ( ph -> B C_ A )
4 1 2 suplub 
 |-  ( ph -> ( ( C e. A /\ C R sup ( B , A , R ) ) -> E. z e. B C R z ) )
5 4 expdimp 
 |-  ( ( ph /\ C e. A ) -> ( C R sup ( B , A , R ) -> E. z e. B C R z ) )
6 breq2 
 |-  ( z = w -> ( C R z <-> C R w ) )
7 6 cbvrexvw 
 |-  ( E. z e. B C R z <-> E. w e. B C R w )
8 breq2 
 |-  ( sup ( B , A , R ) = w -> ( C R sup ( B , A , R ) <-> C R w ) )
9 8 biimprd 
 |-  ( sup ( B , A , R ) = w -> ( C R w -> C R sup ( B , A , R ) ) )
10 9 a1i 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> ( sup ( B , A , R ) = w -> ( C R w -> C R sup ( B , A , R ) ) ) )
11 1 ad2antrr 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> R Or A )
12 simplr 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> C e. A )
13 3 adantr 
 |-  ( ( ph /\ C e. A ) -> B C_ A )
14 13 sselda 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> w e. A )
15 1 2 supcl 
 |-  ( ph -> sup ( B , A , R ) e. A )
16 15 ad2antrr 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> sup ( B , A , R ) e. A )
17 sotr 
 |-  ( ( R Or A /\ ( C e. A /\ w e. A /\ sup ( B , A , R ) e. A ) ) -> ( ( C R w /\ w R sup ( B , A , R ) ) -> C R sup ( B , A , R ) ) )
18 11 12 14 16 17 syl13anc 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> ( ( C R w /\ w R sup ( B , A , R ) ) -> C R sup ( B , A , R ) ) )
19 18 expcomd 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> ( w R sup ( B , A , R ) -> ( C R w -> C R sup ( B , A , R ) ) ) )
20 1 2 supub 
 |-  ( ph -> ( w e. B -> -. sup ( B , A , R ) R w ) )
21 20 adantr 
 |-  ( ( ph /\ C e. A ) -> ( w e. B -> -. sup ( B , A , R ) R w ) )
22 21 imp 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> -. sup ( B , A , R ) R w )
23 sotric 
 |-  ( ( R Or A /\ ( sup ( B , A , R ) e. A /\ w e. A ) ) -> ( sup ( B , A , R ) R w <-> -. ( sup ( B , A , R ) = w \/ w R sup ( B , A , R ) ) ) )
24 11 16 14 23 syl12anc 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> ( sup ( B , A , R ) R w <-> -. ( sup ( B , A , R ) = w \/ w R sup ( B , A , R ) ) ) )
25 24 con2bid 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> ( ( sup ( B , A , R ) = w \/ w R sup ( B , A , R ) ) <-> -. sup ( B , A , R ) R w ) )
26 22 25 mpbird 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> ( sup ( B , A , R ) = w \/ w R sup ( B , A , R ) ) )
27 10 19 26 mpjaod 
 |-  ( ( ( ph /\ C e. A ) /\ w e. B ) -> ( C R w -> C R sup ( B , A , R ) ) )
28 27 rexlimdva 
 |-  ( ( ph /\ C e. A ) -> ( E. w e. B C R w -> C R sup ( B , A , R ) ) )
29 7 28 biimtrid 
 |-  ( ( ph /\ C e. A ) -> ( E. z e. B C R z -> C R sup ( B , A , R ) ) )
30 5 29 impbid 
 |-  ( ( ph /\ C e. A ) -> ( C R sup ( B , A , R ) <-> E. z e. B C R z ) )