Theorem frd

Description: A nonempty subset of an R -well-founded class has an R -minimal element (deduction form). (Contributed by BJ, 16-Nov-2024)

	Ref	Expression
Hypotheses	frd.fr	$$⊢\phi \to R\mathrm{Fr}A$$
	frd.ss	$$⊢\phi \to B\subseteq A$$
	frd.ex	$$⊢\phi \to B\in V$$
	frd.n0	$$⊢\phi \to B\ne \varnothing$$
Assertion	frd	$$⊢\phi \to \exists x\in B\forall y\in B\neg yRx$$

Proof

Step	Hyp	Ref	Expression
1		frd.fr	$$⊢\phi \to R\mathrm{Fr}A$$
2		frd.ss	$$⊢\phi \to B\subseteq A$$
3		frd.ex	$$⊢\phi \to B\in V$$
4		frd.n0	$$⊢\phi \to B\ne \varnothing$$
5		simpr	$$⊢\left(\phi \wedge z=B\right)\to z=B$$
6		biidd	$$⊢\left(\phi \wedge z=B\right)\to \left(\neg yRx\leftrightarrow \neg yRx\right)$$
7	5 6	raleqbidv	$$⊢\left(\phi \wedge z=B\right)\to \left(\forall y\in z\neg yRx\leftrightarrow \forall y\in B\neg yRx\right)$$
8	5 7	rexeqbidv	$$⊢\left(\phi \wedge z=B\right)\to \left(\exists x\in z\forall y\in z\neg yRx\leftrightarrow \exists x\in B\forall y\in B\neg yRx\right)$$
9	3 2	elpwd	$$⊢\phi \to B\in 𝒫A$$
10		nelsn	$$⊢B\ne \varnothing \to \neg B\in \left\{\varnothing \right\}$$
11	4 10	syl	$$⊢\phi \to \neg B\in \left\{\varnothing \right\}$$
12	9 11	eldifd	$$⊢\phi \to B\in \left(𝒫A\setminus \left\{\varnothing \right\}\right)$$
13		dffr6	$$⊢R\mathrm{Fr}A\leftrightarrow \forall z\in \left(𝒫A\setminus \left\{\varnothing \right\}\right)\exists x\in z\forall y\in z\neg yRx$$
14	1 13	sylib	$$⊢\phi \to \forall z\in \left(𝒫A\setminus \left\{\varnothing \right\}\right)\exists x\in z\forall y\in z\neg yRx$$
15	8 12 14	rspcdv2	$$⊢\phi \to \exists x\in B\forall y\in B\neg yRx$$