Theorem bnj106

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

	Ref	Expression
Hypotheses	bnj106.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)$$
	bnj106.2	$$⊢F\in \mathrm{V}$$
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		bnj106.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		bnj106.2	$$⊢F\in \mathrm{V}$$
3		bnj105	$$⊢1_{𝑜}\in \mathrm{V}$$
4	1 3	bnj92	$$⊢\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)$$
5	4	sbcbii	$$⊢\underset{\dot{}}{[}F/f\underset{\dot{}}{]}\underset{\dot{}}{[}{1}_{𝑜}/n\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}F/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)$$
6		fveq1	$$⊢f=F\to f\left(\mathrm{suc}i\right)=F\left(\mathrm{suc}i\right)$$
7		fveq1	$$⊢f=F\to f\left(i\right)=F\left(i\right)$$
8	7	bnj1113	$$⊢f=F\to \bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)$$
9	6 8	eqeq12d	$$⊢f=F\to \left(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)\right)$$
10	9	imbi2d	$$⊢f=F\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 F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
11	10	ralbidv	$$⊢f=F\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 F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
12	2 11	sbcie	$$⊢\underset{\dot{}}{[}F/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 F\left(\mathrm{suc}i\right)=\bigcup _{y\in F\left(i\right)}pred\left(y,A,R\right)\right)$$
13	5 12	bitri	$$⊢\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)$$