Metamath Proof Explorer


Theorem supmo

Description: Any class B has at most one supremum in A (where R is interpreted as 'less than'). (Contributed by NM, 5-May-1999) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis supmo.1
|- ( ph -> R Or A )
Assertion supmo
|- ( 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 ) ) )

Proof

Step Hyp Ref Expression
1 supmo.1
 |-  ( ph -> R Or A )
2 ancom
 |-  ( ( A. y e. B -. x R y /\ A. y e. B -. w R y ) <-> ( A. y e. B -. w R y /\ A. y e. B -. x R y ) )
3 2 anbi2ci
 |-  ( ( ( A. y e. B -. x R y /\ A. y e. B -. w R y ) /\ ( A. y e. A ( y R w -> E. z e. B y R z ) /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) <-> ( ( A. y e. A ( y R w -> E. z e. B y R z ) /\ A. y e. A ( y R x -> E. z e. B y R z ) ) /\ ( A. y e. B -. w R y /\ A. y e. B -. x R y ) ) )
4 an42
 |-  ( ( ( 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 -. w R y /\ A. y e. A ( y R w -> E. z e. B y R z ) ) ) <-> ( ( A. y e. B -. x R y /\ A. y e. B -. w R y ) /\ ( A. y e. A ( y R w -> E. z e. B y R z ) /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
5 an42
 |-  ( ( ( A. y e. A ( y R w -> E. z e. B y R z ) /\ 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 -. w R y ) ) <-> ( ( A. y e. A ( y R w -> E. z e. B y R z ) /\ A. y e. A ( y R x -> E. z e. B y R z ) ) /\ ( A. y e. B -. w R y /\ A. y e. B -. x R y ) ) )
6 3 4 5 3bitr4i
 |-  ( ( ( 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 -. w R y /\ A. y e. A ( y R w -> E. z e. B y R z ) ) ) <-> ( ( A. y e. A ( y R w -> E. z e. B y R z ) /\ 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 -. w R y ) ) )
7 ralnex
 |-  ( A. y e. B -. x R y <-> -. E. y e. B x R y )
8 breq1
 |-  ( y = x -> ( y R w <-> x R w ) )
9 breq1
 |-  ( y = x -> ( y R z <-> x R z ) )
10 9 rexbidv
 |-  ( y = x -> ( E. z e. B y R z <-> E. z e. B x R z ) )
11 8 10 imbi12d
 |-  ( y = x -> ( ( y R w -> E. z e. B y R z ) <-> ( x R w -> E. z e. B x R z ) ) )
12 11 rspcva
 |-  ( ( x e. A /\ A. y e. A ( y R w -> E. z e. B y R z ) ) -> ( x R w -> E. z e. B x R z ) )
13 breq2
 |-  ( y = z -> ( x R y <-> x R z ) )
14 13 cbvrexvw
 |-  ( E. y e. B x R y <-> E. z e. B x R z )
15 12 14 syl6ibr
 |-  ( ( x e. A /\ A. y e. A ( y R w -> E. z e. B y R z ) ) -> ( x R w -> E. y e. B x R y ) )
16 15 con3d
 |-  ( ( x e. A /\ A. y e. A ( y R w -> E. z e. B y R z ) ) -> ( -. E. y e. B x R y -> -. x R w ) )
17 7 16 syl5bi
 |-  ( ( x e. A /\ A. y e. A ( y R w -> E. z e. B y R z ) ) -> ( A. y e. B -. x R y -> -. x R w ) )
18 17 expimpd
 |-  ( x e. A -> ( ( A. y e. A ( y R w -> E. z e. B y R z ) /\ A. y e. B -. x R y ) -> -. x R w ) )
19 18 ad2antrl
 |-  ( ( R Or A /\ ( x e. A /\ w e. A ) ) -> ( ( A. y e. A ( y R w -> E. z e. B y R z ) /\ A. y e. B -. x R y ) -> -. x R w ) )
20 ralnex
 |-  ( A. y e. B -. w R y <-> -. E. y e. B w R y )
21 breq1
 |-  ( y = w -> ( y R x <-> w R x ) )
22 breq1
 |-  ( y = w -> ( y R z <-> w R z ) )
23 22 rexbidv
 |-  ( y = w -> ( E. z e. B y R z <-> E. z e. B w R z ) )
24 21 23 imbi12d
 |-  ( y = w -> ( ( y R x -> E. z e. B y R z ) <-> ( w R x -> E. z e. B w R z ) ) )
25 24 rspcva
 |-  ( ( w e. A /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> ( w R x -> E. z e. B w R z ) )
26 breq2
 |-  ( y = z -> ( w R y <-> w R z ) )
27 26 cbvrexvw
 |-  ( E. y e. B w R y <-> E. z e. B w R z )
28 25 27 syl6ibr
 |-  ( ( w e. A /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> ( w R x -> E. y e. B w R y ) )
29 28 con3d
 |-  ( ( w e. A /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> ( -. E. y e. B w R y -> -. w R x ) )
30 20 29 syl5bi
 |-  ( ( w e. A /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> ( A. y e. B -. w R y -> -. w R x ) )
31 30 expimpd
 |-  ( w e. A -> ( ( A. y e. A ( y R x -> E. z e. B y R z ) /\ A. y e. B -. w R y ) -> -. w R x ) )
32 31 ad2antll
 |-  ( ( R Or A /\ ( x e. A /\ w e. A ) ) -> ( ( A. y e. A ( y R x -> E. z e. B y R z ) /\ A. y e. B -. w R y ) -> -. w R x ) )
33 19 32 anim12d
 |-  ( ( R Or A /\ ( x e. A /\ w e. A ) ) -> ( ( ( A. y e. A ( y R w -> E. z e. B y R z ) /\ 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 -. w R y ) ) -> ( -. x R w /\ -. w R x ) ) )
34 6 33 syl5bi
 |-  ( ( R Or A /\ ( x e. A /\ w 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 -. w R y /\ A. y e. A ( y R w -> E. z e. B y R z ) ) ) -> ( -. x R w /\ -. w R x ) ) )
35 sotrieq2
 |-  ( ( R Or A /\ ( x e. A /\ w e. A ) ) -> ( x = w <-> ( -. x R w /\ -. w R x ) ) )
36 34 35 sylibrd
 |-  ( ( R Or A /\ ( x e. A /\ w 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 -. w R y /\ A. y e. A ( y R w -> E. z e. B y R z ) ) ) -> x = w ) )
37 36 ralrimivva
 |-  ( R Or A -> A. x e. A A. w 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 -. w R y /\ A. y e. A ( y R w -> E. z e. B y R z ) ) ) -> x = w ) )
38 1 37 syl
 |-  ( ph -> A. x e. A A. w 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 -. w R y /\ A. y e. A ( y R w -> E. z e. B y R z ) ) ) -> x = w ) )
39 breq1
 |-  ( x = w -> ( x R y <-> w R y ) )
40 39 notbid
 |-  ( x = w -> ( -. x R y <-> -. w R y ) )
41 40 ralbidv
 |-  ( x = w -> ( A. y e. B -. x R y <-> A. y e. B -. w R y ) )
42 breq2
 |-  ( x = w -> ( y R x <-> y R w ) )
43 42 imbi1d
 |-  ( x = w -> ( ( y R x -> E. z e. B y R z ) <-> ( y R w -> E. z e. B y R z ) ) )
44 43 ralbidv
 |-  ( x = w -> ( A. y e. A ( y R x -> E. z e. B y R z ) <-> A. y e. A ( y R w -> E. z e. B y R z ) ) )
45 41 44 anbi12d
 |-  ( x = w -> ( ( 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 -. w R y /\ A. y e. A ( y R w -> E. z e. B y R z ) ) ) )
46 45 rmo4
 |-  ( 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. x e. A A. w 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 -. w R y /\ A. y e. A ( y R w -> E. z e. B y R z ) ) ) -> x = w ) )
47 38 46 sylibr
 |-  ( 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 ) ) )