Metamath Proof Explorer

Theorem wereu

Description: A nonempty subset of an R -well-ordered class has a unique R -minimal element. (Contributed by NM, 18-Mar-1997) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion wereu 
|- ( ( R We A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> E! x e. B A. y e. B -. y R x )

Proof

Step Hyp Ref Expression
1 wefr 
 |-  ( R We A -> R Fr A )
2 fri 
 |-  ( ( ( B e. V /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
3 2 exp32 
 |-  ( ( B e. V /\ R Fr A ) -> ( B C_ A -> ( B =/= (/) -> E. x e. B A. y e. B -. y R x ) ) )
4 3 expcom 
 |-  ( R Fr A -> ( B e. V -> ( B C_ A -> ( B =/= (/) -> E. x e. B A. y e. B -. y R x ) ) ) )
5 4 3imp2 
 |-  ( ( R Fr A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
6 1 5 sylan 
 |-  ( ( R We A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
7 weso 
 |-  ( R We A -> R Or A )
8 soss 
 |-  ( B C_ A -> ( R Or A -> R Or B ) )
9 7 8 mpan9 
 |-  ( ( R We A /\ B C_ A ) -> R Or B )
10 somo 
 |-  ( R Or B -> E* x e. B A. y e. B -. y R x )
11 9 10 syl 
 |-  ( ( R We A /\ B C_ A ) -> E* x e. B A. y e. B -. y R x )
12 11 3ad2antr2 
 |-  ( ( R We A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> E* x e. B A. y e. B -. y R x )
13 reu5 
 |-  ( E! x e. B A. y e. B -. y R x <-> ( E. x e. B A. y e. B -. y R x /\ E* x e. B A. y e. B -. y R x ) )
14 6 12 13 sylanbrc 
 |-  ( ( R We A /\ ( B e. V /\ B C_ A /\ B =/= (/) ) ) -> E! x e. B A. y e. B -. y R x )