Theorem bnj539

Description: Technical lemma for bnj852 . 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	bnj539.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)$$
	bnj539.2	No typesetting found for |- ( ps' <-> [. M / n ]. ps ) with typecode |-
	bnj539.3	$$⊢M\in \mathrm{V}$$
Assertion	bnj539	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		bnj539.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		bnj539.2	Could not format ( ps' <-> [. M / n ]. ps ) : No typesetting found for |- ( ps' <-> [. M / n ]. ps ) with typecode |-
3		bnj539.3	$$⊢M\in \mathrm{V}$$
4	1	sbcbii	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}M/n\underset{\dot{}}{]}\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)$$
5	3	bnj538	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\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)\leftrightarrow \forall i\in \mathrm{\omega }\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\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)$$
6		sbcimg	$$⊢M\in \mathrm{V}\to \left(\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\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)\leftrightarrow \left(\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\mathrm{suc}i\in n\to \underset{\dot{}}{[}M/n\underset{\dot{}}{]}F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
7	3 6	ax-mp	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\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)\leftrightarrow \left(\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\mathrm{suc}i\in n\to \underset{\dot{}}{[}M/n\underset{\dot{}}{]}F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)$$
8		sbcel2gv	$$⊢M\in \mathrm{V}\to \left(\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\mathrm{suc}i\in n\leftrightarrow \mathrm{suc}i\in M\right)$$
9	3 8	ax-mp	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\mathrm{suc}i\in n\leftrightarrow \mathrm{suc}i\in M$$
10	3	bnj525	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\leftrightarrow F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)$$
11	9 10	imbi12i	$$⊢\left(\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\mathrm{suc}i\in n\to \underset{\dot{}}{[}M/n\underset{\dot{}}{]}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 M\to F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)$$
12	7 11	bitri	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\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)\leftrightarrow \left(\mathrm{suc}i\in M\to F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)$$
13	12	ralbii	$$⊢\forall i\in \mathrm{\omega }\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\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)\leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in M\to F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)$$
14	5 13	bitri	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\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)\leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in M\to F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)$$
15	4 14	bitri	$$⊢\underset{\dot{}}{[}M/n\underset{\dot{}}{]}\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in M\to F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)$$
16	2 15	bitri	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 |-