Theorem wfrlem8

Description: Lemma for well-founded recursion. Compute the prececessor class for an R minimal element of ( A \ dom F ) . (Contributed by Scott Fenton, 21-Apr-2011)

	Ref	Expression
Hypothesis	wfrlem6.1	|- F = wrecs ( R , A , G )
Assertion	wfrlem8	|- ( Pred ( R , ( A \ dom F ) , X ) = (/) <-> Pred ( R , A , X ) = Pred ( R , dom F , X ) )

Proof

Step	Hyp	Ref	Expression
1		wfrlem6.1	|- F = wrecs ( R , A , G )
2	1	wfrdmss	|- dom F C_ A
3		predpredss	|- ( dom F C_ A -> Pred ( R , dom F , X ) C_ Pred ( R , A , X ) )
4	2 3	ax-mp	|- Pred ( R , dom F , X ) C_ Pred ( R , A , X )
5	4	biantru	|- ( Pred ( R , A , X ) C_ Pred ( R , dom F , X ) <-> ( Pred ( R , A , X ) C_ Pred ( R , dom F , X ) /\ Pred ( R , dom F , X ) C_ Pred ( R , A , X ) ) )
6		preddif	|- Pred ( R , ( A \ dom F ) , X ) = ( Pred ( R , A , X ) \ Pred ( R , dom F , X ) )
7	6	eqeq1i	|- ( Pred ( R , ( A \ dom F ) , X ) = (/) <-> ( Pred ( R , A , X ) \ Pred ( R , dom F , X ) ) = (/) )
8		ssdif0	|- ( Pred ( R , A , X ) C_ Pred ( R , dom F , X ) <-> ( Pred ( R , A , X ) \ Pred ( R , dom F , X ) ) = (/) )
9	7 8	bitr4i	|- ( Pred ( R , ( A \ dom F ) , X ) = (/) <-> Pred ( R , A , X ) C_ Pred ( R , dom F , X ) )
10		eqss	|- ( Pred ( R , A , X ) = Pred ( R , dom F , X ) <-> ( Pred ( R , A , X ) C_ Pred ( R , dom F , X ) /\ Pred ( R , dom F , X ) C_ Pred ( R , A , X ) ) )
11	5 9 10	3bitr4i	|- ( Pred ( R , ( A \ dom F ) , X ) = (/) <-> Pred ( R , A , X ) = Pred ( R , dom F , X ) )