Metamath Proof Explorer

Theorem tz6.26

Description: All nonempty subclasses of a class having a well-ordered set-like relation have minimal elements for that relation. Proposition 6.26 of TakeutiZaring p. 31. (Contributed by Scott Fenton, 29-Jan-2011) (Revised by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion tz6.26 
|- ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) )

Proof

Step Hyp Ref Expression
1 wereu2 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E! y e. B A. x e. B -. x R y )
2 reurex 
 |-  ( E! y e. B A. x e. B -. x R y -> E. y e. B A. x e. B -. x R y )
3 1 2 syl 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B A. x e. B -. x R y )
4 rabeq0 
 |-  ( { x e. B | x R y } = (/) <-> A. x e. B -. x R y )
5 dfrab3 
 |-  { x e. B | x R y } = ( B i^i { x | x R y } )
6 vex 
 |-  y e. _V
7 6 dfpred2 
 |-  Pred ( R , B , y ) = ( B i^i { x | x R y } )
8 5 7 eqtr4i 
 |-  { x e. B | x R y } = Pred ( R , B , y )
9 8 eqeq1i 
 |-  ( { x e. B | x R y } = (/) <-> Pred ( R , B , y ) = (/) )
10 4 9 bitr3i 
 |-  ( A. x e. B -. x R y <-> Pred ( R , B , y ) = (/) )
11 10 rexbii 
 |-  ( E. y e. B A. x e. B -. x R y <-> E. y e. B Pred ( R , B , y ) = (/) )
12 3 11 sylib 
 |-  ( ( ( R We A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. y e. B Pred ( R , B , y ) = (/) )