Theorem bnj908

Description: Technical lemma for bnj69 . 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	bnj908.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
	bnj908.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)$$
	bnj908.3	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
	bnj908.4	$$⊢\chi \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
	bnj908.5	$$⊢\theta \leftrightarrow \forall m\in D\left(m\mathrm{E}n\to \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\chi \right)$$
	bnj908.10	No typesetting found for |- ( ph' <-> [. m / n ]. ph ) with typecode |-
	bnj908.11	No typesetting found for |- ( ps' <-> [. m / n ]. ps ) with typecode |-
	bnj908.12	No typesetting found for |- ( ch' <-> [. m / n ]. ch ) with typecode |-
	bnj908.13	No typesetting found for |- ( ph" <-> [. G / f ]. ph ) with typecode |-
	bnj908.14	No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
	bnj908.15	No typesetting found for |- ( ch" <-> [. G / f ]. ch ) with typecode |-
	bnj908.16	$$⊢G=f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}$$
	bnj908.17	No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
	bnj908.18	$$⊢\sigma \leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in m\right)$$
	bnj908.19	$$⊢\eta \leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in \mathrm{\omega }\wedge m=\mathrm{suc}p\right)$$
	bnj908.20	$$⊢\zeta \leftrightarrow \left(i\in \mathrm{\omega }\wedge \mathrm{suc}i\in n\wedge m=\mathrm{suc}i\right)$$
	bnj908.21	$$⊢\rho \leftrightarrow \left(i\in \mathrm{\omega }\wedge \mathrm{suc}i\in n\wedge m\ne \mathrm{suc}i\right)$$
	bnj908.22	$$⊢B=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)$$
	bnj908.23	$$⊢C=\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)$$
	bnj908.24	$$⊢K=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)$$
	bnj908.25	$$⊢L=\bigcup _{y\in G\left(p\right)}pred\left(y,A,R\right)$$
	bnj908.26	$$⊢G=f\cup \left\{⟨m,C⟩\right\}$$
Assertion	bnj908	Could not format assertion : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj908.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
2		bnj908.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		bnj908.3	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
4		bnj908.4	$$⊢\chi \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
5		bnj908.5	$$⊢\theta \leftrightarrow \forall m\in D\left(m\mathrm{E}n\to \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\chi \right)$$
6		bnj908.10	Could not format ( ph' <-> [. m / n ]. ph ) : No typesetting found for |- ( ph' <-> [. m / n ]. ph ) with typecode |-
7		bnj908.11	Could not format ( ps' <-> [. m / n ]. ps ) : No typesetting found for |- ( ps' <-> [. m / n ]. ps ) with typecode |-
8		bnj908.12	Could not format ( ch' <-> [. m / n ]. ch ) : No typesetting found for |- ( ch' <-> [. m / n ]. ch ) with typecode |-
9		bnj908.13	Could not format ( ph" <-> [. G / f ]. ph ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph ) with typecode |-
10		bnj908.14	Could not format ( ps" <-> [. G / f ]. ps ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
11		bnj908.15	Could not format ( ch" <-> [. G / f ]. ch ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch ) with typecode |-
12		bnj908.16	$$⊢G=f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}$$
13		bnj908.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
14		bnj908.18	$$⊢\sigma \leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in m\right)$$
15		bnj908.19	$$⊢\eta \leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in \mathrm{\omega }\wedge m=\mathrm{suc}p\right)$$
16		bnj908.20	$$⊢\zeta \leftrightarrow \left(i\in \mathrm{\omega }\wedge \mathrm{suc}i\in n\wedge m=\mathrm{suc}i\right)$$
17		bnj908.21	$$⊢\rho \leftrightarrow \left(i\in \mathrm{\omega }\wedge \mathrm{suc}i\in n\wedge m\ne \mathrm{suc}i\right)$$
18		bnj908.22	$$⊢B=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)$$
19		bnj908.23	$$⊢C=\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)$$
20		bnj908.24	$$⊢K=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)$$
21		bnj908.25	$$⊢L=\bigcup _{y\in G\left(p\right)}pred\left(y,A,R\right)$$
22		bnj908.26	$$⊢G=f\cup \left\{⟨m,C⟩\right\}$$
23		bnj248	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) ) with typecode |-
24		vex	$$⊢m\in \mathrm{V}$$
25	4 6 7 8 24	bnj207	Could not format ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode |-
26	25	biimpi	Could not format ( ch' -> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ch' -> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode |-
27		euex	Could not format ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
28	26 27	syl6	Could not format ( ch' -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ch' -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode |-
29	28	impcom	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
30	29 13	bnj1198	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ta ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ta ) with typecode |-
31	23 30	bnj832	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ta ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ta ) with typecode |-
32		bnj645	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> et ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> et ) with typecode |-
33		19.41v	$$⊢\exists f\left(\tau \wedge \eta \right)\leftrightarrow \left(\exists f\tau \wedge \eta \right)$$
34	31 32 33	sylanbrc	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( ta /\ et ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( ta /\ et ) ) with typecode |-
35		bnj642	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> R _FrSe A ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> R _FrSe A ) with typecode |-
36		19.41v	$$⊢\exists f\left(\left(\tau \wedge \eta \right)\wedge RFrSeA\right)\leftrightarrow \left(\exists f\left(\tau \wedge \eta \right)\wedge RFrSeA\right)$$
37	34 35 36	sylanbrc	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( ( ta /\ et ) /\ R _FrSe A ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( ( ta /\ et ) /\ R _FrSe A ) ) with typecode |-
38		bnj170	$$⊢\left(RFrSeA\wedge \tau \wedge \eta \right)\leftrightarrow \left(\left(\tau \wedge \eta \right)\wedge RFrSeA\right)$$
39	37 38	bnj1198	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( R _FrSe A /\ ta /\ et ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( R _FrSe A /\ ta /\ et ) ) with typecode |-
40	1 6 24	bnj523	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
41	2 7 24	bnj539	Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
42	40 41 3 12 13 14	bnj544	$$⊢\left(RFrSeA\wedge \tau \wedge \sigma \right)\to GFnn$$
43	14 15 42	bnj561	$$⊢\left(RFrSeA\wedge \tau \wedge \eta \right)\to GFnn$$
44	12	bnj528	$$⊢G\in \mathrm{V}$$
45	1 9 44	bnj609	Could not format ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode |-
46	40 3 12 13 14 42 45	bnj545	Could not format ( ( R _FrSe A /\ ta /\ si ) -> ph" ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ si ) -> ph" ) with typecode |-
47	14 15 46	bnj562	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ph" ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode |-
48	2 10 44	bnj611	Could not format ( ps" <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode |-
49	3 12 13 14 15 16 18 19 20 21 22 40 41 42 17 43 48	bnj571	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ps" ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode |-
50	43 47 49	3jca	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ( G Fn n /\ ph" /\ ps" ) ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ( G Fn n /\ ph" /\ ps" ) ) with typecode |-
51	39 50	bnj593	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) ) with typecode |-