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 ) = (/) )