Theorem frrlem11

Description: Lemma for well-founded recursion. For the next several theorems we will be aiming to prove that dom F = A . To do this, we set up a function C that supposedly contains an element of A that is not in dom F and we show that the element must be in dom F . Our choice of what to restrict F to depends on if we assume partial orders or the axiom of infinity. To begin with, we establish the functionality of C . (Contributed by Scott Fenton, 7-Dec-2022)

	Ref	Expression
Hypotheses	frrlem11.1	|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
	frrlem11.2	|- F = frecs ( R , A , G )
	frrlem11.3	|- ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
	frrlem11.4	|- C = ( ( F |` S ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } )
Assertion	frrlem11	|- ( ( ph /\ z e. ( A \ dom F ) ) -> C Fn ( ( S i^i dom F ) u. { z } ) )

Proof

Step	Hyp	Ref	Expression
1		frrlem11.1	|- B = { f | E. x ( f Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( f ` y ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
2		frrlem11.2	|- F = frecs ( R , A , G )
3		frrlem11.3	|- ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( x g u /\ x h v ) -> u = v ) )
4		frrlem11.4	|- C = ( ( F |` S ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } )
5	1 2 3	frrlem9	|- ( ph -> Fun F )
6	5	funresd	|- ( ph -> Fun ( F |` S ) )
7		dmres	|- dom ( F |` S ) = ( S i^i dom F )
8		df-fn	|- ( ( F |` S ) Fn ( S i^i dom F ) <-> ( Fun ( F |` S ) /\ dom ( F |` S ) = ( S i^i dom F ) ) )
9	7 8	mpbiran2	|- ( ( F |` S ) Fn ( S i^i dom F ) <-> Fun ( F |` S ) )
10	6 9	sylibr	|- ( ph -> ( F |` S ) Fn ( S i^i dom F ) )
11		vex	|- z e. _V
12		ovex	|- ( z G ( F |` Pred ( R , A , z ) ) ) e. _V
13	11 12	fnsn	|- { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } Fn { z }
14	10 13	jctir	|- ( ph -> ( ( F |` S ) Fn ( S i^i dom F ) /\ { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } Fn { z } ) )
15		eldifn	|- ( z e. ( A \ dom F ) -> -. z e. dom F )
16		elinel2	|- ( z e. ( S i^i dom F ) -> z e. dom F )
17	15 16	nsyl	|- ( z e. ( A \ dom F ) -> -. z e. ( S i^i dom F ) )
18		disjsn	|- ( ( ( S i^i dom F ) i^i { z } ) = (/) <-> -. z e. ( S i^i dom F ) )
19	17 18	sylibr	|- ( z e. ( A \ dom F ) -> ( ( S i^i dom F ) i^i { z } ) = (/) )
20		fnun	|- ( ( ( ( F |` S ) Fn ( S i^i dom F ) /\ { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } Fn { z } ) /\ ( ( S i^i dom F ) i^i { z } ) = (/) ) -> ( ( F |` S ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) Fn ( ( S i^i dom F ) u. { z } ) )
21	14 19 20	syl2an	|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( ( F |` S ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) Fn ( ( S i^i dom F ) u. { z } ) )
22	4	fneq1i	|- ( C Fn ( ( S i^i dom F ) u. { z } ) <-> ( ( F |` S ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) Fn ( ( S i^i dom F ) u. { z } ) )
23	21 22	sylibr	|- ( ( ph /\ z e. ( A \ dom F ) ) -> C Fn ( ( S i^i dom F ) u. { z } ) )