Theorem bnj155

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	bnj155.1	No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
	bnj155.2	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 |-
Assertion	bnj155	Could not format assertion : No typesetting found for |- ( ps1 <-> A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj155.1	Could not format ( ps1 <-> [. g / f ]. ps' ) : No typesetting found for |- ( ps1 <-> [. g / f ]. ps' ) with typecode |-
2		bnj155.2	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 |-
3	2	sbcbii	Could not format ( [. g / f ]. ps' <-> [. g / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( [. g / f ]. ps' <-> [. g / f ]. A. i e. _om ( suc i e. 1o -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
4		vex	$$⊢g\in \mathrm{V}$$
5		fveq1	$$⊢f=g\to f\left(\mathrm{suc}i\right)=g\left(\mathrm{suc}i\right)$$
6		fveq1	$$⊢f=g\to f\left(i\right)=g\left(i\right)$$
7	6	iuneq1d	$$⊢f=g\to \bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)=\bigcup _{y\in g\left(i\right)}pred\left(y,A,R\right)$$
8	5 7	eqeq12d	$$⊢f=g\to \left(f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\leftrightarrow g\left(\mathrm{suc}i\right)=\bigcup _{y\in g\left(i\right)}pred\left(y,A,R\right)\right)$$
9	8	imbi2d	$$⊢f=g\to \left(\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)\leftrightarrow \left(\mathrm{suc}i\in 1_{𝑜}\to g\left(\mathrm{suc}i\right)=\bigcup _{y\in g\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
10	9	ralbidv	$$⊢f=g\to \left(\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)\leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in 1_{𝑜}\to g\left(\mathrm{suc}i\right)=\bigcup _{y\in g\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
11	4 10	sbcie	$$⊢\underset{\dot{}}{[}g/f\underset{\dot{}}{]}\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)\leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in 1_{𝑜}\to g\left(\mathrm{suc}i\right)=\bigcup _{y\in g\left(i\right)}pred\left(y,A,R\right)\right)$$
12	1 3 11	3bitri	Could not format ( ps1 <-> A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps1 <-> A. i e. _om ( suc i e. 1o -> ( g ` suc i ) = U_ y e. ( g ` i ) _pred ( y , A , R ) ) ) with typecode |-