Theorem bnj126

Description: Technical lemma for bnj150 . 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	bnj126.1	$$⊢\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)$$
	bnj126.2	No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
	bnj126.3	No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
	bnj126.4	$$⊢F=\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
Assertion	bnj126	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		bnj126.1	$$⊢\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)$$
2		bnj126.2	Could not format ( ps' <-> [. 1o / n ]. ps ) : No typesetting found for |- ( ps' <-> [. 1o / n ]. ps ) with typecode |-
3		bnj126.3	Could not format ( ps" <-> [. F / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. F / f ]. ps' ) with typecode |-
4		bnj126.4	$$⊢F=\left\{⟨\varnothing ,pred\left(x,A,R\right)⟩\right\}$$
5	2	sbcbii	Could not format ( [. F / f ]. ps' <-> [. F / f ]. [. 1o / n ]. ps ) : No typesetting found for |- ( [. F / f ]. ps' <-> [. F / f ]. [. 1o / n ]. ps ) with typecode |-
6	4	bnj95	$$⊢F\in \mathrm{V}$$
7	1 6	bnj106	$$⊢\underset{\dot{}}{[}F/f\underset{\dot{}}{]}\underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\psi \leftrightarrow \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)$$
8	3 5 7	3bitri	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 |-