This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrrid 
 |-  ( R Fr A -> ( E. x e. A ph -> E. x e. A ( ph /\ A. y e. A ( ps -> -. y R x ) ) ) )