Theorem bnj151

Description: Technical lemma for bnj153 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj151.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
	bnj151.2	$$⊢\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in n\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
	bnj151.3	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
	bnj151.4	$$⊢\theta \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
	bnj151.5	$$⊢\tau \leftrightarrow \forall m\in D\left(m\mathrm{E}n\to \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\theta \right)$$
	bnj151.6	$$⊢\zeta \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \left(fFnn\wedge \phi \wedge \psi \right)\right)$$
	bnj151.7	No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
	bnj151.8	No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
	bnj151.9	No typesetting found for |- ( th' <-> [. 1o / n ]. th ) with typecode |-
	bnj151.10	No typesetting found for |- ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
	bnj151.11	No typesetting found for |- ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
	bnj151.12	No typesetting found for |- ( ze' <-> [. 1o / n ]. ze ) with typecode |-
	bnj151.13	$$⊢F=\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
	bnj151.14	No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
	bnj151.15	No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
	bnj151.16	No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |-
	bnj151.17	No typesetting found for |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
	bnj151.18	No typesetting found for |- ( ze1 <-> [. g / f ]. ze0 ) with typecode |-
	bnj151.19	No typesetting found for |- ( ph1 <-> [. g / f ]. ph' ) with typecode |-
	bnj151.20	No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
Assertion	bnj151	$$⊢n=1_{𝑜}\to \left(\left(n\in D\wedge \tau \right)\to \theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		bnj151.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
2		bnj151.2	$$⊢\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in n\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
3		bnj151.3	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
4		bnj151.4	$$⊢\theta \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
5		bnj151.5	$$⊢\tau \leftrightarrow \forall m\in D\left(m\mathrm{E}n\to \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\theta \right)$$
6		bnj151.6	$$⊢\zeta \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \left(fFnn\wedge \phi \wedge \psi \right)\right)$$
7		bnj151.7	Could not format ( ph' <-> [. 1o / n ]. ph ) : No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
8		bnj151.8	Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
9		bnj151.9	Could not format ( th' <-> [. 1o / n ]. th ) : No typesetting found for |- ( th' <-> [. 1o / n ]. th ) with typecode |-
10		bnj151.10	Could not format ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
11		bnj151.11	Could not format ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( th1 <-> ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
12		bnj151.12	Could not format ( ze' <-> [. 1o / n ]. ze ) : No typesetting found for |- ( ze' <-> [. 1o / n ]. ze ) with typecode |-
13		bnj151.13	$$⊢F=\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
14		bnj151.14	Could not format ( ph" <-> [. F / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
15		bnj151.15	Could not format ( ps" <-> [. F / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
16		bnj151.16	Could not format ( ze" <-> [. F / f ]. ze' ) : No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |-
17		bnj151.17	Could not format ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( ze0 <-> ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
18		bnj151.18	Could not format ( ze1 <-> [. g / f ]. ze0 ) : No typesetting found for |- ( ze1 <-> [. g / f ]. ze0 ) with typecode |-
19		bnj151.19	Could not format ( ph1 <-> [. g / f ]. ph' ) : No typesetting found for |- ( ph1 <-> [. g / f ]. ph' ) with typecode |-
20		bnj151.20	Could not format ( ps1 <-> [. g / f ]. ps' ) : No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
21	1 2 6 7 8 10 12 13 14 15 16	bnj150	Could not format th0 : No typesetting found for |- th0 with typecode |-
22	21 10	mpbi	Could not format ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
23	1 7	bnj118	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
24	11 17 18 19 20 23	bnj149	Could not format th1 : No typesetting found for |- th1 with typecode |-
25	24 11	mpbi	Could not format ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> E* f ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
26		df-eu	Could not format ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> ( E. f ( f Fn 1o /\ ph' /\ ps' ) /\ E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( E! f ( f Fn 1o /\ ph' /\ ps' ) <-> ( E. f ( f Fn 1o /\ ph' /\ ps' ) /\ E* f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
27	22 25 26	sylanbrc	Could not format ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) with typecode |-
28	4 7 8 9	bnj130	Could not format ( th' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( th' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
29	27 28	mpbir	Could not format th' : No typesetting found for |- th' with typecode |-
30		sbceq1a	$$⊢n=1_{𝑜}\to \left(\theta \leftrightarrow \underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\theta \right)$$
31	30 9	bitr4di	Could not format ( n = 1o -> ( th <-> th' ) ) : No typesetting found for |- ( n = 1o -> ( th <-> th' ) ) with typecode |-
32	29 31	mpbiri	$$⊢n=1_{𝑜}\to \theta$$
33	32	a1d	$$⊢n=1_{𝑜}\to \left(\left(n\in D\wedge \tau \right)\to \theta \right)$$