Theorem frr1

Description: Law of general well-founded recursion, part one. This theorem and the following two drop the partial order requirement from fpr1 , fpr2 , and fpr3 , which requires using the axiom of infinity (Contributed by Scott Fenton, 11-Sep-2023)

	Ref	Expression
Hypothesis	frr.1	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
Assertion	frr1	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\to FFnA$$

Proof

Step	Hyp	Ref	Expression
1		frr.1	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
2		eqid	$$⊢\left\{a|\exists b\left(aFnb\wedge \left(b\subseteq A\wedge \forall c\in bPred\left(R,A,c\right)\subseteq b\right)\wedge \forall c\in ba\left(c\right)=cG\left({a\upharpoonright }_{Pred\left(R,A,c\right)}\right)\right)\right\}=\left\{a|\exists b\left(aFnb\wedge \left(b\subseteq A\wedge \forall c\in bPred\left(R,A,c\right)\subseteq b\right)\wedge \forall c\in ba\left(c\right)=cG\left({a\upharpoonright }_{Pred\left(R,A,c\right)}\right)\right)\right\}$$
3	2	frrlem1	$$⊢\left\{a|\exists b\left(aFnb\wedge \left(b\subseteq A\wedge \forall c\in bPred\left(R,A,c\right)\subseteq b\right)\wedge \forall c\in ba\left(c\right)=cG\left({a\upharpoonright }_{Pred\left(R,A,c\right)}\right)\right)\right\}=\left\{f|\exists x\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=yG\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
4	3 1	frrlem15	$$⊢\left(\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\wedge \left(g\in \left\{a|\exists b\left(aFnb\wedge \left(b\subseteq A\wedge \forall c\in bPred\left(R,A,c\right)\subseteq b\right)\wedge \forall c\in ba\left(c\right)=cG\left({a\upharpoonright }_{Pred\left(R,A,c\right)}\right)\right)\right\}\wedge h\in \left\{a|\exists b\left(aFnb\wedge \left(b\subseteq A\wedge \forall c\in bPred\left(R,A,c\right)\subseteq b\right)\wedge \forall c\in ba\left(c\right)=cG\left({a\upharpoonright }_{Pred\left(R,A,c\right)}\right)\right)\right\}\right)\right)\to \left(\left(xgu\wedge xhv\right)\to u=v\right)$$
5	3 1 4	frrlem9	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\to \mathrm{Fun}F$$
6		eqid	Could not format ( ( F |` Pred ( t++ ( R |` A ) , A , z ) ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) = ( ( F |` Pred ( t++ ( R |` A ) , A , z ) ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) : No typesetting found for |- ( ( F |` Pred ( t++ ( R |` A ) , A , z ) ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) = ( ( F |` Pred ( t++ ( R |` A ) , A , z ) ) u. { <. z , ( z G ( F |` Pred ( R , A , z ) ) ) >. } ) with typecode |-
7		simpl	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\to R\mathrm{Fr}A$$
8		predres	$$⊢Pred\left(R,A,z\right)=Pred\left(\left({R\upharpoonright }_A\right),A,z\right)$$
9		relres	$$⊢\mathrm{Rel}\left({R\upharpoonright }_A\right)$$
10		ssttrcl	Could not format ( Rel ( R |` A ) -> ( R |` A ) C_ t++ ( R |` A ) ) : No typesetting found for |- ( Rel ( R |` A ) -> ( R |` A ) C_ t++ ( R |` A ) ) with typecode |-
11		predrelss	Could not format ( ( R |` A ) C_ t++ ( R |` A ) -> Pred ( ( R |` A ) , A , z ) C_ Pred ( t++ ( R |` A ) , A , z ) ) : No typesetting found for |- ( ( R |` A ) C_ t++ ( R |` A ) -> Pred ( ( R |` A ) , A , z ) C_ Pred ( t++ ( R |` A ) , A , z ) ) with typecode |-
12	9 10 11	mp2b	Could not format Pred ( ( R |` A ) , A , z ) C_ Pred ( t++ ( R |` A ) , A , z ) : No typesetting found for |- Pred ( ( R |` A ) , A , z ) C_ Pred ( t++ ( R |` A ) , A , z ) with typecode |-
13	8 12	eqsstri	Could not format Pred ( R , A , z ) C_ Pred ( t++ ( R |` A ) , A , z ) : No typesetting found for |- Pred ( R , A , z ) C_ Pred ( t++ ( R |` A ) , A , z ) with typecode |-
14	13	a1i	Could not format ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( R , A , z ) C_ Pred ( t++ ( R |` A ) , A , z ) ) : No typesetting found for |- ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( R , A , z ) C_ Pred ( t++ ( R |` A ) , A , z ) ) with typecode |-
15		frrlem16	Could not format ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> A. a e. Pred ( t++ ( R |` A ) , A , z ) Pred ( R , A , a ) C_ Pred ( t++ ( R |` A ) , A , z ) ) : No typesetting found for |- ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> A. a e. Pred ( t++ ( R |` A ) , A , z ) Pred ( R , A , a ) C_ Pred ( t++ ( R |` A ) , A , z ) ) with typecode |-
16		ttrclse	Could not format ( R Se A -> t++ ( R |` A ) Se A ) : No typesetting found for |- ( R Se A -> t++ ( R |` A ) Se A ) with typecode |-
17		setlikespec	Could not format ( ( z e. A /\ t++ ( R |` A ) Se A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V ) : No typesetting found for |- ( ( z e. A /\ t++ ( R |` A ) Se A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V ) with typecode |-
18	17	ancoms	Could not format ( ( t++ ( R |` A ) Se A /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V ) : No typesetting found for |- ( ( t++ ( R |` A ) Se A /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V ) with typecode |-
19	16 18	sylan	Could not format ( ( R Se A /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V ) : No typesetting found for |- ( ( R Se A /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V ) with typecode |-
20	19	adantll	Could not format ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V ) : No typesetting found for |- ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) e. _V ) with typecode |-
21		predss	Could not format Pred ( t++ ( R |` A ) , A , z ) C_ A : No typesetting found for |- Pred ( t++ ( R |` A ) , A , z ) C_ A with typecode |-
22	21	a1i	Could not format ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) C_ A ) : No typesetting found for |- ( ( ( R Fr A /\ R Se A ) /\ z e. A ) -> Pred ( t++ ( R |` A ) , A , z ) C_ A ) with typecode |-
23		difss	$$⊢A\setminus \mathrm{dom}F\subseteq A$$
24		frmin	$$⊢\left(\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\wedge \left(A\setminus \mathrm{dom}F\subseteq A\wedge A\setminus \mathrm{dom}F\ne \varnothing \right)\right)\to \exists z\in \left(A\setminus \mathrm{dom}F\right)Pred\left(R,\left(A\setminus \mathrm{dom}F\right),z\right)=\varnothing$$
25	23 24	mpanr1	$$⊢\left(\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\wedge A\setminus \mathrm{dom}F\ne \varnothing \right)\to \exists z\in \left(A\setminus \mathrm{dom}F\right)Pred\left(R,\left(A\setminus \mathrm{dom}F\right),z\right)=\varnothing$$
26	3 1 4 6 7 14 15 20 22 25	frrlem14	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\to \mathrm{dom}F=A$$
27		df-fn	$$⊢FFnA\leftrightarrow \left(\mathrm{Fun}F\wedge \mathrm{dom}F=A\right)$$
28	5 26 27	sylanbrc	$$⊢\left(R\mathrm{Fr}A\wedge R\mathrm{Se}A\right)\to FFnA$$