Theorem bnj999

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	bnj999.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(X,A,R\right)$$
	bnj999.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)$$
	bnj999.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
	bnj999.7	No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
	bnj999.8	No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
	bnj999.9	No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
	bnj999.10	No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
	bnj999.11	No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
	bnj999.12	No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
	bnj999.15	$$⊢C=\bigcup _{y\in f\left(m\right)}pred\left(y,A,R\right)$$
	bnj999.16	$$⊢G=f\cup \left\{⟨n,C⟩\right\}$$
Assertion	bnj999	Could not format assertion : No typesetting found for |- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj999.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(X,A,R\right)$$
2		bnj999.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		bnj999.3	$$⊢\chi \leftrightarrow \left(n\in D\wedge fFnn\wedge \phi \wedge \psi \right)$$
4		bnj999.7	Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
5		bnj999.8	Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
6		bnj999.9	Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
7		bnj999.10	Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
8		bnj999.11	Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
9		bnj999.12	Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
10		bnj999.15	$$⊢C=\bigcup _{y\in f\left(m\right)}pred\left(y,A,R\right)$$
11		bnj999.16	$$⊢G=f\cup \left\{⟨n,C⟩\right\}$$
12		vex	$$⊢p\in \mathrm{V}$$
13	3 4 5 6 12	bnj919	Could not format ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) ) : No typesetting found for |- ( ch' <-> ( p e. D /\ f Fn p /\ ph' /\ ps' ) ) with typecode |-
14	11	bnj918	$$⊢G\in \mathrm{V}$$
15	13 7 8 9 14	bnj976	Could not format ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for |- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode |-
16	15	bnj1254	Could not format ( ch" -> ps" ) : No typesetting found for |- ( ch" -> ps" ) with typecode |-
17	16	anim1i	Could not format ( ( ch" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) -> ( ps" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) : No typesetting found for |- ( ( ch" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) -> ( ps" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) with typecode |-
18		bnj252	Could not format ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ch" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) : No typesetting found for |- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ch" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) with typecode |-
19		bnj252	Could not format ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ps" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) : No typesetting found for |- ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) <-> ( ps" /\ ( i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) ) with typecode |-
20	17 18 19	3imtr4i	Could not format ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) : No typesetting found for |- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) ) with typecode |-
21		ssiun2	$$⊢y\in G\left(i\right)\to pred\left(y,A,R\right)\subseteq \bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)$$
22	21	bnj708	Could not format ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ U_ y e. ( G ` i ) _pred ( y , A , R ) ) : No typesetting found for |- ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ U_ y e. ( G ` i ) _pred ( y , A , R ) ) with typecode |-
23		3simpa	Could not format ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( ps" /\ i e. _om ) ) : No typesetting found for |- ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( ps" /\ i e. _om ) ) with typecode |-
24	23	ancomd	Could not format ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( i e. _om /\ ps" ) ) : No typesetting found for |- ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( i e. _om /\ ps" ) ) with typecode |-
25		simp3	Could not format ( ( ps" /\ i e. _om /\ suc i e. p ) -> suc i e. p ) : No typesetting found for |- ( ( ps" /\ i e. _om /\ suc i e. p ) -> suc i e. p ) with typecode |-
26	2 5 12	bnj539	Could not format ( ps' <-> A. i e. _om ( suc i e. p -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. p -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
27	26 8 10 11	bnj965	Could not format ( ps" <-> A. i e. _om ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode |-
28	27	bnj228	Could not format ( ( i e. _om /\ ps" ) -> ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ( i e. _om /\ ps" ) -> ( suc i e. p -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode |-
29	24 25 28	sylc	Could not format ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) : No typesetting found for |- ( ( ps" /\ i e. _om /\ suc i e. p ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) with typecode |-
30	29	bnj721	Could not format ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) : No typesetting found for |- ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) with typecode |-
31	22 30	sseqtrrd	Could not format ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) : No typesetting found for |- ( ( ps" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) with typecode |-
32	20 31	syl	Could not format ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) : No typesetting found for |- ( ( ch" /\ i e. _om /\ suc i e. p /\ y e. ( G ` i ) ) -> _pred ( y , A , R ) C_ ( G ` suc i ) ) with typecode |-