Theorem wfrlem10

Description: Lemma for well-founded recursion. When z is an R minimal element of ( A \ dom F ) , then its predecessor class is equal to dom F . (Contributed by Scott Fenton, 21-Apr-2011)

	Ref	Expression
Hypotheses	wfrlem10.1	|- R We A
	wfrlem10.2	|- F = wrecs ( R , A , G )
Assertion	wfrlem10	|- ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> Pred ( R , A , z ) = dom F )

Proof

Step	Hyp	Ref	Expression
1		wfrlem10.1	|- R We A
2		wfrlem10.2	|- F = wrecs ( R , A , G )
3	2	wfrlem8	|- ( Pred ( R , ( A \ dom F ) , z ) = (/) <-> Pred ( R , A , z ) = Pred ( R , dom F , z ) )
4	3	biimpi	|- ( Pred ( R , ( A \ dom F ) , z ) = (/) -> Pred ( R , A , z ) = Pred ( R , dom F , z ) )
5		predss	|- Pred ( R , dom F , z ) C_ dom F
6	5	a1i	|- ( z e. ( A \ dom F ) -> Pred ( R , dom F , z ) C_ dom F )
7		simpr	|- ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> w e. dom F )
8		eldifn	|- ( z e. ( A \ dom F ) -> -. z e. dom F )
9		eleq1w	|- ( w = z -> ( w e. dom F <-> z e. dom F ) )
10	9	notbid	|- ( w = z -> ( -. w e. dom F <-> -. z e. dom F ) )
11	8 10	syl5ibrcom	|- ( z e. ( A \ dom F ) -> ( w = z -> -. w e. dom F ) )
12	11	con2d	|- ( z e. ( A \ dom F ) -> ( w e. dom F -> -. w = z ) )
13	12	imp	|- ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> -. w = z )
14		ssel	|- ( Pred ( R , A , w ) C_ dom F -> ( z e. Pred ( R , A , w ) -> z e. dom F ) )
15	14	con3d	|- ( Pred ( R , A , w ) C_ dom F -> ( -. z e. dom F -> -. z e. Pred ( R , A , w ) ) )
16	8 15	syl5com	|- ( z e. ( A \ dom F ) -> ( Pred ( R , A , w ) C_ dom F -> -. z e. Pred ( R , A , w ) ) )
17	2	wfrdmcl	|- ( w e. dom F -> Pred ( R , A , w ) C_ dom F )
18	16 17	impel	|- ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> -. z e. Pred ( R , A , w ) )
19		eldifi	|- ( z e. ( A \ dom F ) -> z e. A )
20		elpredg	|- ( ( w e. dom F /\ z e. A ) -> ( z e. Pred ( R , A , w ) <-> z R w ) )
21	20	ancoms	|- ( ( z e. A /\ w e. dom F ) -> ( z e. Pred ( R , A , w ) <-> z R w ) )
22	19 21	sylan	|- ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> ( z e. Pred ( R , A , w ) <-> z R w ) )
23	18 22	mtbid	|- ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> -. z R w )
24	2	wfrdmss	|- dom F C_ A
25	24	sseli	|- ( w e. dom F -> w e. A )
26		weso	|- ( R We A -> R Or A )
27	1 26	ax-mp	|- R Or A
28		solin	|- ( ( R Or A /\ ( w e. A /\ z e. A ) ) -> ( w R z \/ w = z \/ z R w ) )
29	27 28	mpan	|- ( ( w e. A /\ z e. A ) -> ( w R z \/ w = z \/ z R w ) )
30	25 19 29	syl2anr	|- ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> ( w R z \/ w = z \/ z R w ) )
31	13 23 30	ecase23d	|- ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> w R z )
32		vex	|- w e. _V
33	32	elpred	|- ( z e. _V -> ( w e. Pred ( R , dom F , z ) <-> ( w e. dom F /\ w R z ) ) )
34	33	elv	|- ( w e. Pred ( R , dom F , z ) <-> ( w e. dom F /\ w R z ) )
35	7 31 34	sylanbrc	|- ( ( z e. ( A \ dom F ) /\ w e. dom F ) -> w e. Pred ( R , dom F , z ) )
36	6 35	eqelssd	|- ( z e. ( A \ dom F ) -> Pred ( R , dom F , z ) = dom F )
37	4 36	sylan9eqr	|- ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> Pred ( R , A , z ) = dom F )