Theorem bnj150

Description: Technical lemma for bnj151 . 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	bnj150.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
	bnj150.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)$$
	bnj150.3	$$⊢\zeta \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \left(fFnn\wedge \phi \wedge \psi \right)\right)$$
	bnj150.4	No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
	bnj150.5	No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
	bnj150.6	No typesetting found for |- ( th0 <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
	bnj150.7	No typesetting found for |- ( ze' <-> [. 1o / n ]. ze ) with typecode |-
	bnj150.8	$$⊢F=\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
	bnj150.9	No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
	bnj150.10	No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
	bnj150.11	No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |-
Assertion	bnj150	Could not format assertion : No typesetting found for |- th0 with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj150.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
2		bnj150.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		bnj150.3	$$⊢\zeta \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \left(fFnn\wedge \phi \wedge \psi \right)\right)$$
4		bnj150.4	Could not format ( ph' <-> [. 1o / n ]. ph ) : No typesetting found for |- ( ph' <-> [. 1o / n ]. ph ) with typecode |-
5		bnj150.5	Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
6		bnj150.6	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 |-
7		bnj150.7	Could not format ( ze' <-> [. 1o / n ]. ze ) : No typesetting found for |- ( ze' <-> [. 1o / n ]. ze ) with typecode |-
8		bnj150.8	$$⊢F=\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
9		bnj150.9	Could not format ( ph" <-> [. F / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. F / f ]. ph' ) with typecode |-
10		bnj150.10	Could not format ( ps" <-> [. F / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
11		bnj150.11	Could not format ( ze" <-> [. F / f ]. ze' ) : No typesetting found for |- ( ze" <-> [. F / f ]. ze' ) with typecode |-
12	8	bnj95	$$⊢F\in \mathrm{V}$$
13		sbceq1a	Could not format ( f = F -> ( ze' <-> [. F / f ]. ze' ) ) : No typesetting found for |- ( f = F -> ( ze' <-> [. F / f ]. ze' ) ) with typecode |-
14	13 11	bitr4di	Could not format ( f = F -> ( ze' <-> ze" ) ) : No typesetting found for |- ( f = F -> ( ze' <-> ze" ) ) with typecode |-
15		0ex	$$⊢\varnothing \in \mathrm{V}$$
16		bnj93	$$⊢\left(RFrSeA\wedge x\in A\right)\to pred\left(x,A,R\right)\in \mathrm{V}$$
17		funsng	$$⊢\left(\varnothing \in \mathrm{V}\wedge pred\left(x,A,R\right)\in \mathrm{V}\right)\to \mathrm{Fun}\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
18	15 16 17	sylancr	$$⊢\left(RFrSeA\wedge x\in A\right)\to \mathrm{Fun}\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
19	8	funeqi	$$⊢\mathrm{Fun}F\leftrightarrow \mathrm{Fun}\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
20	18 19	sylibr	$$⊢\left(RFrSeA\wedge x\in A\right)\to \mathrm{Fun}F$$
21	8	bnj96	$$⊢\left(RFrSeA\wedge x\in A\right)\to \mathrm{dom}F=1_{𝑜}$$
22	20 21	bnj1422	$$⊢\left(RFrSeA\wedge x\in A\right)\to FFn{1}_{𝑜}$$
23	8	bnj97	$$⊢\left(RFrSeA\wedge x\in A\right)\to F\left(\varnothing \right)=pred\left(x,A,R\right)$$
24	1 4 9 8	bnj125	Could not format ( ph" <-> ( F ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph" <-> ( F ` (/) ) = _pred ( x , A , R ) ) with typecode |-
25	23 24	sylibr	Could not format ( ( R _FrSe A /\ x e. A ) -> ph" ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> ph" ) with typecode |-
26	22 25	jca	Could not format ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" ) ) with typecode |-
27		bnj98	$$⊢\forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in 1_{𝑜}\to F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)$$
28	2 5 10 8	bnj126	Could not format ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) ) ) with typecode |-
29	27 28	mpbir	Could not format ps" : No typesetting found for |- ps" with typecode |-
30		df-3an	Could not format ( ( F Fn 1o /\ ph" /\ ps" ) <-> ( ( F Fn 1o /\ ph" ) /\ ps" ) ) : No typesetting found for |- ( ( F Fn 1o /\ ph" /\ ps" ) <-> ( ( F Fn 1o /\ ph" ) /\ ps" ) ) with typecode |-
31	26 29 30	sylanblrc	Could not format ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) with typecode |-
32	3 7 4 5	bnj121	Could not format ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ze' <-> ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
33	8 9 10 11 32	bnj124	Could not format ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ze" <-> ( ( R _FrSe A /\ x e. A ) -> ( F Fn 1o /\ ph" /\ ps" ) ) ) with typecode |-
34	31 33	mpbir	Could not format ze" : No typesetting found for |- ze" with typecode |-
35	12 14 34	ceqsexv2d	Could not format E. f ze' : No typesetting found for |- E. f ze' with typecode |-
36		19.37v	Could not format ( E. f ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( E. f ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) <-> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
37	6 36	bitr4i	Could not format ( th0 <-> E. f ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( th0 <-> E. f ( ( R _FrSe A /\ x e. A ) -> ( f Fn 1o /\ ph' /\ ps' ) ) ) with typecode |-
38	37 32	bnj133	Could not format ( th0 <-> E. f ze' ) : No typesetting found for |- ( th0 <-> E. f ze' ) with typecode |-
39	35 38	mpbir	Could not format th0 : No typesetting found for |- th0 with typecode |-