Theorem frrlem11

Description: Lemma for 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 ordering or Infinity. To begin with, we establish the functionhood 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		funres	|- ( Fun F -> Fun ( F |` S ) )
7	5 6	syl	|- ( ph -> Fun ( F |` S ) )
8		dmres	|- dom ( F |` S ) = ( S i^i dom F )
9		df-fn	|- ( ( F |` S ) Fn ( S i^i dom F ) <-> ( Fun ( F |` S ) /\ dom ( F |` S ) = ( S i^i dom F ) ) )
10	8 9	mpbiran2	|- ( ( F |` S ) Fn ( S i^i dom F ) <-> Fun ( F |` S ) )
11	7 10	sylibr	|- ( ph -> ( F |` S ) Fn ( S i^i dom F ) )
12		vex	|- z e. _V
13		ovex	|- ( z G ( F |` Pred ( R , A , z ) ) ) e. _V
14	12 13	fnsn	|- { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } Fn { z }
15	11 14	jctir	|- ( ph -> ( ( F |` S ) Fn ( S i^i dom F ) /\ { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } Fn { z } ) )
16		eldifn	|- ( z e. ( A \ dom F ) -> -. z e. dom F )
17		elinel2	|- ( z e. ( S i^i dom F ) -> z e. dom F )
18	16 17	nsyl	|- ( z e. ( A \ dom F ) -> -. z e. ( S i^i dom F ) )
19		disjsn	|- ( ( ( S i^i dom F ) i^i { z } ) = (/) <-> -. z e. ( S i^i dom F ) )
20	18 19	sylibr	|- ( z e. ( A \ dom F ) -> ( ( S i^i dom F ) i^i { z } ) = (/) )
21		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 } ) )
22	15 20 21	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 } ) )
23	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 } ) )
24	22 23	sylibr	|- ( ( ph /\ z e. ( A \ dom F ) ) -> C Fn ( ( S i^i dom F ) u. { z } ) )