Theorem wfrlem13

Description: Lemma for well-founded recursion. From here through wfrlem16 , we aim to prove that dom F = A . We do this by supposing that there is an element z of A that is not in dom F . We then define C by extending dom F with the appropriate value at z . We then show that z cannot be an R minimal element of ( A \ dom F ) , meaning that ( A \ dom F ) must be empty, so dom F = A . Here, we show that C is a function extending the domain of F by one. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	wfrlem13.1	|- R We A
	wfrlem13.2	|- R Se A
	wfrlem13.3	|- F = wrecs ( R , A , G )
	wfrlem13.4	|- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
Assertion	wfrlem13	|- ( z e. ( A \ dom F ) -> C Fn ( dom F u. { z } ) )

Proof

Step	Hyp	Ref	Expression
1		wfrlem13.1	|- R We A
2		wfrlem13.2	|- R Se A
3		wfrlem13.3	|- F = wrecs ( R , A , G )
4		wfrlem13.4	|- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
5	1 2 3	wfrfun	|- Fun F
6		vex	|- z e. _V
7		fvex	|- ( G ` ( F |` Pred ( R , A , z ) ) ) e. _V
8	6 7	funsn	|- Fun { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. }
9	5 8	pm3.2i	|- ( Fun F /\ Fun { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
10	7	dmsnop	|- dom { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } = { z }
11	10	ineq2i	|- ( dom F i^i dom { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) = ( dom F i^i { z } )
12		eldifn	|- ( z e. ( A \ dom F ) -> -. z e. dom F )
13		disjsn	|- ( ( dom F i^i { z } ) = (/) <-> -. z e. dom F )
14	12 13	sylibr	|- ( z e. ( A \ dom F ) -> ( dom F i^i { z } ) = (/) )
15	11 14	syl5eq	|- ( z e. ( A \ dom F ) -> ( dom F i^i dom { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) = (/) )
16		funun	|- ( ( ( Fun F /\ Fun { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) /\ ( dom F i^i dom { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) = (/) ) -> Fun ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) )
17	9 15 16	sylancr	|- ( z e. ( A \ dom F ) -> Fun ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) )
18		dmun	|- dom ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) = ( dom F u. dom { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
19	10	uneq2i	|- ( dom F u. dom { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) = ( dom F u. { z } )
20	18 19	eqtri	|- dom ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) = ( dom F u. { z } )
21	4	fneq1i	|- ( C Fn ( dom F u. { z } ) <-> ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) Fn ( dom F u. { z } ) )
22		df-fn	|- ( ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) Fn ( dom F u. { z } ) <-> ( Fun ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) /\ dom ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) = ( dom F u. { z } ) ) )
23	21 22	bitri	|- ( C Fn ( dom F u. { z } ) <-> ( Fun ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) /\ dom ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) = ( dom F u. { z } ) ) )
24	17 20 23	sylanblrc	|- ( z e. ( A \ dom F ) -> C Fn ( dom F u. { z } ) )