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 } ) )

Metamath Proof Explorer

Theorem frrlem11

Proof