frrlem12

Description: Lemma for well-founded recursion. Next, we calculate the value 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 ) ) ) >. } )
	frrlem12.5	\|- ( ph -> R Fr A )
	frrlem12.6	\|- ( ( ph /\ z e. A ) -> Pred ( R , A , z ) C_ S )
	frrlem12.7	\|- ( ( ph /\ z e. A ) -> A. w e. S Pred ( R , A , w ) C_ S )
Assertion	frrlem12	\|- ( ( ph /\ z e. ( A \ dom F ) /\ w e. ( ( S i^i dom F ) u. { z } ) ) -> ( C ` w ) = ( w G ( C \|` Pred ( R , A , w ) ) ) )

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		frrlem12.5	\|- ( ph -> R Fr A )
6		frrlem12.6	\|- ( ( ph /\ z e. A ) -> Pred ( R , A , z ) C_ S )
7		frrlem12.7	\|- ( ( ph /\ z e. A ) -> A. w e. S Pred ( R , A , w ) C_ S )
8		elun	\|- ( w e. ( ( S i^i dom F ) u. { z } ) <-> ( w e. ( S i^i dom F ) \/ w e. { z } ) )
9		velsn	\|- ( w e. { z } <-> w = z )
10	9	orbi2i	\|- ( ( w e. ( S i^i dom F ) \/ w e. { z } ) <-> ( w e. ( S i^i dom F ) \/ w = z ) )
11	8 10	bitri	\|- ( w e. ( ( S i^i dom F ) u. { z } ) <-> ( w e. ( S i^i dom F ) \/ w = z ) )
12		elinel2	\|- ( w e. ( S i^i dom F ) -> w e. dom F )
13	1	frrlem1	\|- B = { p \| E. q ( p Fn q /\ ( q C_ A /\ A. w e. q Pred ( R , A , w ) C_ q ) /\ A. w e. q ( p ` w ) = ( w G ( p \|` Pred ( R , A , w ) ) ) ) }
14		breq1	\|- ( x = q -> ( x g u <-> q g u ) )
15		breq1	\|- ( x = q -> ( x h v <-> q h v ) )
16	14 15	anbi12d	\|- ( x = q -> ( ( x g u /\ x h v ) <-> ( q g u /\ q h v ) ) )
17	16	imbi1d	\|- ( x = q -> ( ( ( x g u /\ x h v ) -> u = v ) <-> ( ( q g u /\ q h v ) -> u = v ) ) )
18	17	imbi2d	\|- ( x = q -> ( ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( x g u /\ x h v ) -> u = v ) ) <-> ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( q g u /\ q h v ) -> u = v ) ) ) )
19	18 3	chvarvv	\|- ( ( ph /\ ( g e. B /\ h e. B ) ) -> ( ( q g u /\ q h v ) -> u = v ) )
20	13 2 19	frrlem10	\|- ( ( ph /\ w e. dom F ) -> ( F ` w ) = ( w G ( F \|` Pred ( R , A , w ) ) ) )
21	12 20	sylan2	\|- ( ( ph /\ w e. ( S i^i dom F ) ) -> ( F ` w ) = ( w G ( F \|` Pred ( R , A , w ) ) ) )
22	21	adantlr	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( F ` w ) = ( w G ( F \|` Pred ( R , A , w ) ) ) )
23	4	fveq1i	\|- ( C ` w ) = ( ( ( F \|` S ) u. { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ) ` w )
24	1 2 3	frrlem9	\|- ( ph -> Fun F )
25	24	funresd	\|- ( ph -> Fun ( F \|` S ) )
26		dmres	\|- dom ( F \|` S ) = ( S i^i dom F )
27		df-fn	\|- ( ( F \|` S ) Fn ( S i^i dom F ) <-> ( Fun ( F \|` S ) /\ dom ( F \|` S ) = ( S i^i dom F ) ) )
28	25 26 27	sylanblrc	\|- ( ph -> ( F \|` S ) Fn ( S i^i dom F ) )
29	28	adantr	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( F \|` S ) Fn ( S i^i dom F ) )
30	29	adantr	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( F \|` S ) Fn ( S i^i dom F ) )
31		vex	\|- z e. _V
32		ovex	\|- ( z G ( F \|` Pred ( R , A , z ) ) ) e. _V
33	31 32	fnsn	\|- { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } Fn { z }
34	33	a1i	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } Fn { z } )
35		eldifn	\|- ( z e. ( A \ dom F ) -> -. z e. dom F )
36		elinel2	\|- ( z e. ( S i^i dom F ) -> z e. dom F )
37	35 36	nsyl	\|- ( z e. ( A \ dom F ) -> -. z e. ( S i^i dom F ) )
38		disjsn	\|- ( ( ( S i^i dom F ) i^i { z } ) = (/) <-> -. z e. ( S i^i dom F ) )
39	37 38	sylibr	\|- ( z e. ( A \ dom F ) -> ( ( S i^i dom F ) i^i { z } ) = (/) )
40	39	adantl	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( ( S i^i dom F ) i^i { z } ) = (/) )
41	40	adantr	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( ( S i^i dom F ) i^i { z } ) = (/) )
42		simpr	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> w e. ( S i^i dom F ) )
43		fvun1	\|- ( ( ( 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 } ) = (/) /\ w e. ( S i^i dom F ) ) ) -> ( ( ( F \|` S ) u. { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ) ` w ) = ( ( F \|` S ) ` w ) )
44	30 34 41 42 43	syl112anc	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( ( ( F \|` S ) u. { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ) ` w ) = ( ( F \|` S ) ` w ) )
45	23 44	eqtrid	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( C ` w ) = ( ( F \|` S ) ` w ) )
46		elinel1	\|- ( w e. ( S i^i dom F ) -> w e. S )
47	46	adantl	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> w e. S )
48	47	fvresd	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( ( F \|` S ) ` w ) = ( F ` w ) )
49	45 48	eqtrd	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( C ` w ) = ( F ` w ) )
50	1 2 3 4	frrlem11	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> C Fn ( ( S i^i dom F ) u. { z } ) )
51		fnfun	\|- ( C Fn ( ( S i^i dom F ) u. { z } ) -> Fun C )
52	50 51	syl	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> Fun C )
53	52	adantr	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> Fun C )
54		ssun1	\|- ( F \|` S ) C_ ( ( F \|` S ) u. { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } )
55	54 4	sseqtrri	\|- ( F \|` S ) C_ C
56	55	a1i	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( F \|` S ) C_ C )
57		eldifi	\|- ( z e. ( A \ dom F ) -> z e. A )
58	57 7	sylan2	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> A. w e. S Pred ( R , A , w ) C_ S )
59		rspa	\|- ( ( A. w e. S Pred ( R , A , w ) C_ S /\ w e. S ) -> Pred ( R , A , w ) C_ S )
60	58 46 59	syl2an	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> Pred ( R , A , w ) C_ S )
61	1 2	frrlem8	\|- ( w e. dom F -> Pred ( R , A , w ) C_ dom F )
62	12 61	syl	\|- ( w e. ( S i^i dom F ) -> Pred ( R , A , w ) C_ dom F )
63	62	adantl	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> Pred ( R , A , w ) C_ dom F )
64	60 63	ssind	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> Pred ( R , A , w ) C_ ( S i^i dom F ) )
65	64 26	sseqtrrdi	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> Pred ( R , A , w ) C_ dom ( F \|` S ) )
66		fun2ssres	\|- ( ( Fun C /\ ( F \|` S ) C_ C /\ Pred ( R , A , w ) C_ dom ( F \|` S ) ) -> ( C \|` Pred ( R , A , w ) ) = ( ( F \|` S ) \|` Pred ( R , A , w ) ) )
67	53 56 65 66	syl3anc	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( C \|` Pred ( R , A , w ) ) = ( ( F \|` S ) \|` Pred ( R , A , w ) ) )
68	60	resabs1d	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( ( F \|` S ) \|` Pred ( R , A , w ) ) = ( F \|` Pred ( R , A , w ) ) )
69	67 68	eqtrd	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( C \|` Pred ( R , A , w ) ) = ( F \|` Pred ( R , A , w ) ) )
70	69	oveq2d	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( w G ( C \|` Pred ( R , A , w ) ) ) = ( w G ( F \|` Pred ( R , A , w ) ) ) )
71	22 49 70	3eqtr4d	\|- ( ( ( ph /\ z e. ( A \ dom F ) ) /\ w e. ( S i^i dom F ) ) -> ( C ` w ) = ( w G ( C \|` Pred ( R , A , w ) ) ) )
72	71	ex	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( w e. ( S i^i dom F ) -> ( C ` w ) = ( w G ( C \|` Pred ( R , A , w ) ) ) ) )
73	31 32	fvsn	\|- ( { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ` z ) = ( z G ( F \|` Pred ( R , A , z ) ) )
74	4	fveq1i	\|- ( C ` z ) = ( ( ( F \|` S ) u. { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ) ` z )
75	33	a1i	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } Fn { z } )
76		vsnid	\|- z e. { z }
77	76	a1i	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> z e. { z } )
78		fvun2	\|- ( ( ( 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 } ) = (/) /\ z e. { z } ) ) -> ( ( ( F \|` S ) u. { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ) ` z ) = ( { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ` z ) )
79	29 75 40 77 78	syl112anc	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( ( ( F \|` S ) u. { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ) ` z ) = ( { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ` z ) )
80	74 79	eqtrid	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( C ` z ) = ( { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ` z ) )
81	4	reseq1i	\|- ( C \|` Pred ( R , A , z ) ) = ( ( ( F \|` S ) u. { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ) \|` Pred ( R , A , z ) )
82		resundir	\|- ( ( ( F \|` S ) u. { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } ) \|` Pred ( R , A , z ) ) = ( ( ( F \|` S ) \|` Pred ( R , A , z ) ) u. ( { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } \|` Pred ( R , A , z ) ) )
83	81 82	eqtri	\|- ( C \|` Pred ( R , A , z ) ) = ( ( ( F \|` S ) \|` Pred ( R , A , z ) ) u. ( { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } \|` Pred ( R , A , z ) ) )
84	57 6	sylan2	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> Pred ( R , A , z ) C_ S )
85	84	resabs1d	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( ( F \|` S ) \|` Pred ( R , A , z ) ) = ( F \|` Pred ( R , A , z ) ) )
86		predfrirr	\|- ( R Fr A -> -. z e. Pred ( R , A , z ) )
87	5 86	syl	\|- ( ph -> -. z e. Pred ( R , A , z ) )
88	87	adantr	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> -. z e. Pred ( R , A , z ) )
89		ressnop0	\|- ( -. z e. Pred ( R , A , z ) -> ( { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } \|` Pred ( R , A , z ) ) = (/) )
90	88 89	syl	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } \|` Pred ( R , A , z ) ) = (/) )
91	85 90	uneq12d	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( ( ( F \|` S ) \|` Pred ( R , A , z ) ) u. ( { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } \|` Pred ( R , A , z ) ) ) = ( ( F \|` Pred ( R , A , z ) ) u. (/) ) )
92		un0	\|- ( ( F \|` Pred ( R , A , z ) ) u. (/) ) = ( F \|` Pred ( R , A , z ) )
93	91 92	eqtrdi	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( ( ( F \|` S ) \|` Pred ( R , A , z ) ) u. ( { <. z , ( z G ( F \|` Pred ( R , A , z ) ) ) >. } \|` Pred ( R , A , z ) ) ) = ( F \|` Pred ( R , A , z ) ) )
94	83 93	eqtrid	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( C \|` Pred ( R , A , z ) ) = ( F \|` Pred ( R , A , z ) ) )
95	94	oveq2d	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( z G ( C \|` Pred ( R , A , z ) ) ) = ( z G ( F \|` Pred ( R , A , z ) ) ) )
96	73 80 95	3eqtr4a	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( C ` z ) = ( z G ( C \|` Pred ( R , A , z ) ) ) )
97		fveq2	\|- ( w = z -> ( C ` w ) = ( C ` z ) )
98		id	\|- ( w = z -> w = z )
99		predeq3	\|- ( w = z -> Pred ( R , A , w ) = Pred ( R , A , z ) )
100	99	reseq2d	\|- ( w = z -> ( C \|` Pred ( R , A , w ) ) = ( C \|` Pred ( R , A , z ) ) )
101	98 100	oveq12d	\|- ( w = z -> ( w G ( C \|` Pred ( R , A , w ) ) ) = ( z G ( C \|` Pred ( R , A , z ) ) ) )
102	97 101	eqeq12d	\|- ( w = z -> ( ( C ` w ) = ( w G ( C \|` Pred ( R , A , w ) ) ) <-> ( C ` z ) = ( z G ( C \|` Pred ( R , A , z ) ) ) ) )
103	96 102	syl5ibrcom	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( w = z -> ( C ` w ) = ( w G ( C \|` Pred ( R , A , w ) ) ) ) )
104	72 103	jaod	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( ( w e. ( S i^i dom F ) \/ w = z ) -> ( C ` w ) = ( w G ( C \|` Pred ( R , A , w ) ) ) ) )
105	11 104	biimtrid	\|- ( ( ph /\ z e. ( A \ dom F ) ) -> ( w e. ( ( S i^i dom F ) u. { z } ) -> ( C ` w ) = ( w G ( C \|` Pred ( R , A , w ) ) ) ) )
106	105	3impia	\|- ( ( ph /\ z e. ( A \ dom F ) /\ w e. ( ( S i^i dom F ) u. { z } ) ) -> ( C ` w ) = ( w G ( C \|` Pred ( R , A , w ) ) ) )

Metamath Proof Explorer

Theorem frrlem12

Proof