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 )