Theorem bnj92

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj92.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)$$
	bnj92.2	$$⊢Z\in \mathrm{V}$$
Assertion	bnj92	$$⊢\underset{\dot{}}{[}Z/n\underset{\dot{}}{]}\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in Z\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		bnj92.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		bnj92.2	$$⊢Z\in \mathrm{V}$$
3	1	sbcbii	$$⊢\underset{\dot{}}{[}Z/n\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}Z/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)$$
4	2	bnj538	$$⊢\underset{\dot{}}{[}Z/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{}}{[}Z/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)$$
5		sbcimg	$$⊢Z\in \mathrm{V}\to \left(\underset{\dot{}}{[}Z/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{}}{[}Z/n\underset{\dot{}}{]}\mathrm{suc}i\in n\to \underset{\dot{}}{[}Z/n\underset{\dot{}}{]}f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
6	2 5	ax-mp	$$⊢\underset{\dot{}}{[}Z/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{}}{[}Z/n\underset{\dot{}}{]}\mathrm{suc}i\in n\to \underset{\dot{}}{[}Z/n\underset{\dot{}}{]}f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
7		sbcel2gv	$$⊢Z\in \mathrm{V}\to \left(\underset{\dot{}}{[}Z/n\underset{\dot{}}{]}\mathrm{suc}i\in n\leftrightarrow \mathrm{suc}i\in Z\right)$$
8	2 7	ax-mp	$$⊢\underset{\dot{}}{[}Z/n\underset{\dot{}}{]}\mathrm{suc}i\in n\leftrightarrow \mathrm{suc}i\in Z$$
9	2	bnj525	$$⊢\underset{\dot{}}{[}Z/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)$$
10	8 9	imbi12i	$$⊢\left(\underset{\dot{}}{[}Z/n\underset{\dot{}}{]}\mathrm{suc}i\in n\to \underset{\dot{}}{[}Z/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 Z\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
11	6 10	bitri	$$⊢\underset{\dot{}}{[}Z/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 Z\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
12	11	ralbii	$$⊢\forall i\in \mathrm{\omega }\underset{\dot{}}{[}Z/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 Z\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
13	3 4 12	3bitri	$$⊢\underset{\dot{}}{[}Z/n\underset{\dot{}}{]}\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in Z\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$