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	|- ( ph -> R Fr A )
	frd.ss	|- ( ph -> B C_ A )
	frd.ex	|- ( ph -> B e. V )
	frd.n0	|- ( ph -> B =/= (/) )
Assertion	frd	|- ( ph -> E. x e. B A. y e. B -. y R x )

Proof

Step	Hyp	Ref	Expression
1		frd.fr	|- ( ph -> R Fr A )
2		frd.ss	|- ( ph -> B C_ A )
3		frd.ex	|- ( ph -> B e. V )
4		frd.n0	|- ( ph -> B =/= (/) )
5		simpr	|- ( ( ph /\ z = B ) -> z = B )
6		biidd	|- ( ( ph /\ z = B ) -> ( -. y R x <-> -. y R x ) )
7	5 6	raleqbidv	|- ( ( ph /\ z = B ) -> ( A. y e. z -. y R x <-> A. y e. B -. y R x ) )
8	5 7	rexeqbidv	|- ( ( ph /\ z = B ) -> ( E. x e. z A. y e. z -. y R x <-> E. x e. B A. y e. B -. y R x ) )
9	3 2	elpwd	|- ( ph -> B e. ~P A )
10		nelsn	|- ( B =/= (/) -> -. B e. { (/) } )
11	4 10	syl	|- ( ph -> -. B e. { (/) } )
12	9 11	eldifd	|- ( ph -> B e. ( ~P A \ { (/) } ) )
13		dffr6	|- ( R Fr A <-> A. z e. ( ~P A \ { (/) } ) E. x e. z A. y e. z -. y R x )
14	1 13	sylib	|- ( ph -> A. z e. ( ~P A \ { (/) } ) E. x e. z A. y e. z -. y R x )
15	8 12 14	rspcdv2	|- ( ph -> E. x e. B A. y e. B -. y R x )