This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frpomin2

Description: Every nonempty (possibly proper) subclass of a class A with a well-founded set-like partial order R has a minimal element. The additional condition of partial order over frmin enables avoiding the axiom of 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 ) = (/) )