Metamath Proof Explorer

Theorem frpomin2

Description: Every (possibly proper) subclass of a class A with a founded, partial-ordering, set-like relation R has a minimal element. The additional condition of partial ordering over frmin enables avoiding infinity. (Contributed by Scott Fenton, 11-Feb-2022)

Ref Expression
Assertion frpomin2 
|- ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B Pred ( R , B , x ) = (/) )

Proof

Step Hyp Ref Expression
1 frpomin 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )
2 vex 
 |-  x e. _V
3 2 dfpred3 
 |-  Pred ( R , B , x ) = { y e. B | y R x }
4 3 eqeq1i 
 |-  ( Pred ( R , B , x ) = (/) <-> { y e. B | y R x } = (/) )
5 rabeq0 
 |-  ( { y e. B | y R x } = (/) <-> A. y e. B -. y R x )
6 4 5 bitri 
 |-  ( Pred ( R , B , x ) = (/) <-> A. y e. B -. y R x )
7 6 rexbii 
 |-  ( E. x e. B Pred ( R , B , x ) = (/) <-> E. x e. B A. y e. B -. y R x )
8 1 7 sylibr 
 |-  ( ( ( R Fr A /\ R Po A /\ R Se A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B Pred ( R , B , x ) = (/) )