Metamath Proof Explorer

Theorem infmo

Description: Any class B has at most one infimum in A (where R is interpreted as 'less than'). (Contributed by AV, 6-Oct-2020)

Ref Expression
Hypothesis infmo.1 
|- ( ph -> R Or A )
Assertion infmo 
|- ( ph -> E* x e. A ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )

Proof

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