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 ) ) ) )