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

Metamath Proof Explorer

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 )