Metamath Proof Explorer

Theorem welb

Description: A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion welb 
|- ( ( R We A /\ ( B e. C /\ 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 wess 
 |-  ( B C_ A -> ( R We A -> R We B ) )
2 1 impcom 
 |-  ( ( R We A /\ B C_ A ) -> R We B )
3 weso 
 |-  ( R We B -> R Or B )
4 2 3 syl 
 |-  ( ( R We A /\ B C_ A ) -> R Or B )
5 cnvso 
 |-  ( R Or B <-> `' R Or B )
6 4 5 sylib 
 |-  ( ( R We A /\ B C_ A ) -> `' R Or B )
7 6 3ad2antr2 
 |-  ( ( R We A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> `' R Or B )
8 wefr 
 |-  ( R We B -> R Fr B )
9 2 8 syl 
 |-  ( ( R We A /\ B C_ A ) -> R Fr B )
10 9 3ad2antr2 
 |-  ( ( R We A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> R Fr B )
11 ssidd 
 |-  ( B C_ A -> B C_ B )
12 11 3anim2i 
 |-  ( ( B e. C /\ B C_ A /\ B =/= (/) ) -> ( B e. C /\ B C_ B /\ B =/= (/) ) )
13 12 adantl 
 |-  ( ( R We A /\ ( B e. C /\ B C_ A /\ B =/= (/) ) ) -> ( B e. C /\ B C_ B /\ B =/= (/) ) )
14 frinfm 
 |-  ( ( R Fr B /\ ( B e. C /\ B C_ B /\ 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 ) ) )
15 10 13 14 syl2anc 
 |-  ( ( R We A /\ ( B e. C /\ B C_ A /\ 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 ) ) )
16 7 15 jca 
 |-  ( ( R We A /\ ( B e. C /\ 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 ) ) ) )