Metamath Proof Explorer

Theorem weinflb

Description: In a well-order, an infimum is a lower bound. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Hypotheses weinflb.1 
|- ( ph -> Rel R )
weinflb.2 
|- ( ph -> R We A )
weinflb.3 
|- ( ph -> B e. V )
weinflb.4 
|- ( ph -> B C_ A )
weinflb.5 
|- ( ph -> B =/= (/) )
weinflb.6 
|- ( ph -> C e. B )
Assertion weinflb 
|- ( ph -> -. C R inf ( B , A , R ) )

Proof

Step Hyp Ref Expression
1 weinflb.1 
 |-  ( ph -> Rel R )
2 weinflb.2 
 |-  ( ph -> R We A )
3 weinflb.3 
 |-  ( ph -> B e. V )
4 weinflb.4 
 |-  ( ph -> B C_ A )
5 weinflb.5 
 |-  ( ph -> B =/= (/) )
6 weinflb.6 
 |-  ( ph -> C e. B )
7 weso 
 |-  ( R We A -> R Or A )
8 2 7 syl 
 |-  ( ph -> R Or A )
9 welb 
 |-  ( ( R We A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> ( `' R Or B /\ E. x e. B ( A. y e. B -. x `' R y /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) ) )
10 2 3 4 5 9 syl13anc 
 |-  ( ph -> ( `' R Or B /\ E. x e. B ( A. y e. B -. x `' R y /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) ) )
11 10 simprd 
 |-  ( ph -> E. x e. B ( A. y e. B -. x `' R y /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) )
12 4 sselda 
 |-  ( ( ph /\ x e. B ) -> x e. A )
13 12 adantrr 
 |-  ( ( ph /\ ( x e. B /\ ( A. y e. B -. x `' R y /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) ) ) -> x e. A )
14 brcnvg 
 |-  ( ( x e. B /\ y e. B ) -> ( x `' R y <-> y R x ) )
15 14 notbid 
 |-  ( ( x e. B /\ y e. B ) -> ( -. x `' R y <-> -. y R x ) )
16 15 ralbidva 
 |-  ( x e. B -> ( A. y e. B -. x `' R y <-> A. y e. B -. y R x ) )
17 16 biimpa 
 |-  ( ( x e. B /\ A. y e. B -. x `' R y ) -> A. y e. B -. y R x )
18 17 adantll 
 |-  ( ( ( ph /\ x e. B ) /\ A. y e. B -. x `' R y ) -> A. y e. B -. y R x )
19 breq1 
 |-  ( z = x -> ( z R y <-> x R y ) )
20 simpllr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. A ) /\ x R y ) -> x e. B )
21 simpr 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. A ) /\ x R y ) -> x R y )
22 19 20 21 rspcedvdw 
 |-  ( ( ( ( ph /\ x e. B ) /\ y e. A ) /\ x R y ) -> E. z e. B z R y )
23 22 ex 
 |-  ( ( ( ph /\ x e. B ) /\ y e. A ) -> ( x R y -> E. z e. B z R y ) )
24 23 ralrimiva 
 |-  ( ( ph /\ x e. B ) -> A. y e. A ( x R y -> E. z e. B z R y ) )
25 24 adantr 
 |-  ( ( ( ph /\ x e. B ) /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) -> A. y e. A ( x R y -> E. z e. B z R y ) )
26 18 25 anim12dan 
 |-  ( ( ( ph /\ x e. B ) /\ ( A. y e. B -. x `' R y /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) ) -> ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
27 26 anasss 
 |-  ( ( ph /\ ( x e. B /\ ( A. y e. B -. x `' R y /\ A. y e. B ( y `' R x -> E. z e. B y `' R z ) ) ) ) -> ( A. y e. B -. y R x /\ A. y e. A ( x R y -> E. z e. B z R y ) ) )
28 11 13 27 reximssdv 
 |-  ( 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 ) ) )
29 8 28 inflb 
 |-  ( ph -> ( C e. B -> -. C R inf ( B , A , R ) ) )
30 6 29 mpd 
 |-  ( ph -> -. C R inf ( B , A , R ) )