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	$$⊢\left(\left(R\mathrm{Fr}A\wedge R\mathrm{Po}A\wedge R\mathrm{Se}A\right)\wedge \left(B\subseteq A\wedge B\ne \varnothing \right)\right)\to \exists x\in BPred\left(R,B,x\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		frpomin	$$⊢\left(\left(R\mathrm{Fr}A\wedge R\mathrm{Po}A\wedge R\mathrm{Se}A\right)\wedge \left(B\subseteq A\wedge B\ne \varnothing \right)\right)\to \exists x\in B\forall y\in B\neg yRx$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	dfpred3	$$⊢Pred\left(R,B,x\right)=\left\{y\in B|yRx\right\}$$
4	3	eqeq1i	$$⊢Pred\left(R,B,x\right)=\varnothing \leftrightarrow \left\{y\in B|yRx\right\}=\varnothing$$
5		rabeq0	$$⊢\left\{y\in B|yRx\right\}=\varnothing \leftrightarrow \forall y\in B\neg yRx$$
6	4 5	bitri	$$⊢Pred\left(R,B,x\right)=\varnothing \leftrightarrow \forall y\in B\neg yRx$$
7	6	rexbii	$$⊢\exists x\in BPred\left(R,B,x\right)=\varnothing \leftrightarrow \exists x\in B\forall y\in B\neg yRx$$
8	1 7	sylibr	$$⊢\left(\left(R\mathrm{Fr}A\wedge R\mathrm{Po}A\wedge R\mathrm{Se}A\right)\wedge \left(B\subseteq A\wedge B\ne \varnothing \right)\right)\to \exists x\in BPred\left(R,B,x\right)=\varnothing$$