Theorem frminex

Description: If an element of a well-founded set satisfies a property ph , then there is a minimal element that satisfies ph . (Contributed by Jeff Madsen, 18-Jun-2010) (Proof shortened by Mario Carneiro, 18-Nov-2016)

	Ref	Expression
Hypotheses	frminex.1	|- A e. _V
	frminex.2	|- ( x = y -> ( ph <-> ps ) )
Assertion	frminex	|- ( R Fr A -> ( E. x e. A ph -> E. x e. A ( ph /\ A. y e. A ( ps -> -. y R x ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		frminex.1	|- A e. _V
2		frminex.2	|- ( x = y -> ( ph <-> ps ) )
3		rabn0	|- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )
4	1	rabex	|- { x e. A | ph } e. _V
5		ssrab2	|- { x e. A | ph } C_ A
6		fri	|- ( ( ( { x e. A | ph } e. _V /\ R Fr A ) /\ ( { x e. A | ph } C_ A /\ { x e. A | ph } =/= (/) ) ) -> E. z e. { x e. A | ph } A. y e. { x e. A | ph } -. y R z )
7	2	ralrab	|- ( A. y e. { x e. A | ph } -. y R z <-> A. y e. A ( ps -> -. y R z ) )
8	7	rexbii	|- ( E. z e. { x e. A | ph } A. y e. { x e. A | ph } -. y R z <-> E. z e. { x e. A | ph } A. y e. A ( ps -> -. y R z ) )
9		breq2	|- ( z = x -> ( y R z <-> y R x ) )
10	9	notbid	|- ( z = x -> ( -. y R z <-> -. y R x ) )
11	10	imbi2d	|- ( z = x -> ( ( ps -> -. y R z ) <-> ( ps -> -. y R x ) ) )
12	11	ralbidv	|- ( z = x -> ( A. y e. A ( ps -> -. y R z ) <-> A. y e. A ( ps -> -. y R x ) ) )
13	12	rexrab2	|- ( E. z e. { x e. A | ph } A. y e. A ( ps -> -. y R z ) <-> E. x e. A ( ph /\ A. y e. A ( ps -> -. y R x ) ) )
14	8 13	bitri	|- ( E. z e. { x e. A | ph } A. y e. { x e. A | ph } -. y R z <-> E. x e. A ( ph /\ A. y e. A ( ps -> -. y R x ) ) )
15	6 14	sylib	|- ( ( ( { x e. A | ph } e. _V /\ R Fr A ) /\ ( { x e. A | ph } C_ A /\ { x e. A | ph } =/= (/) ) ) -> E. x e. A ( ph /\ A. y e. A ( ps -> -. y R x ) ) )
16	15	an4s	|- ( ( ( { x e. A | ph } e. _V /\ { x e. A | ph } C_ A ) /\ ( R Fr A /\ { x e. A | ph } =/= (/) ) ) -> E. x e. A ( ph /\ A. y e. A ( ps -> -. y R x ) ) )
17	4 5 16	mpanl12	|- ( ( R Fr A /\ { x e. A | ph } =/= (/) ) -> E. x e. A ( ph /\ A. y e. A ( ps -> -. y R x ) ) )
18	17	ex	|- ( R Fr A -> ( { x e. A | ph } =/= (/) -> E. x e. A ( ph /\ A. y e. A ( ps -> -. y R x ) ) ) )
19	3 18	syl5bir	|- ( R Fr A -> ( E. x e. A ph -> E. x e. A ( ph /\ A. y e. A ( ps -> -. y R x ) ) ) )