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

Metamath Proof Explorer

Theorem bnj1228

Description: Existence of a minimal element in certain classes: if R is well-founded and set-like on A , then every nonempty subclass of A has a minimal element. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1228.1 
|- ( w e. B -> A. x w e. B )
Assertion bnj1228 
|- ( ( R _FrSe A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x )

Proof

Step Hyp Ref Expression
1 bnj1228.1 
 |-  ( w e. B -> A. x w e. B )
2 bnj69 
 |-  ( ( R _FrSe A /\ B C_ A /\ B =/= (/) ) -> E. z e. B A. y e. B -. y R z )
3 nfv 
 |-  F/ z ( x e. B /\ A. y e. B -. y R x )
4 1 nfcii 
 |-  F/_ x B
5 4 nfcri 
 |-  F/ x z e. B
6 nfv 
 |-  F/ x -. y R z
7 4 6 nfralw 
 |-  F/ x A. y e. B -. y R z
8 5 7 nfan 
 |-  F/ x ( z e. B /\ A. y e. B -. y R z )
9 eleq1w 
 |-  ( x = z -> ( x e. B <-> z e. B ) )
10 breq2 
 |-  ( x = z -> ( y R x <-> y R z ) )
11 10 notbid 
 |-  ( x = z -> ( -. y R x <-> -. y R z ) )
12 11 ralbidv 
 |-  ( x = z -> ( A. y e. B -. y R x <-> A. y e. B -. y R z ) )
13 9 12 anbi12d 
 |-  ( x = z -> ( ( x e. B /\ A. y e. B -. y R x ) <-> ( z e. B /\ A. y e. B -. y R z ) ) )
14 3 8 13 cbvexv1 
 |-  ( E. x ( x e. B /\ A. y e. B -. y R x ) <-> E. z ( z e. B /\ A. y e. B -. y R z ) )
15 df-rex 
 |-  ( E. x e. B A. y e. B -. y R x <-> E. x ( x e. B /\ A. y e. B -. y R x ) )
16 df-rex 
 |-  ( E. z e. B A. y e. B -. y R z <-> E. z ( z e. B /\ A. y e. B -. y R z ) )
17 14 15 16 3bitr4i 
 |-  ( E. x e. B A. y e. B -. y R x <-> E. z e. B A. y e. B -. y R z )
18 2 17 sylibr 
 |-  ( ( R _FrSe A /\ B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x )