Theorem bnj611

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	bnj611.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)$$
	bnj611.2	No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
	bnj611.3	$$⊢G\in \mathrm{V}$$
Assertion	bnj611	Could not format assertion : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		bnj611.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		bnj611.2	Could not format ( ps" <-> [. G / f ]. ps ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
3		bnj611.3	$$⊢G\in \mathrm{V}$$
4		df-ral	$$⊢\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\left(i\in \mathrm{\omega }\to \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)\right)$$
5	4	bicomi	$$⊢\forall i\left(i\in \mathrm{\omega }\to \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)\right)\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)$$
6	5	sbcbii	$$⊢\underset{\dot{}}{[}G/f\underset{\dot{}}{]}\forall i\left(i\in \mathrm{\omega }\to \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)\right)\leftrightarrow \underset{\dot{}}{[}G/f\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)$$
7		nfv	$$⊢Ⅎfi\in \mathrm{\omega }$$
8	7	sbc19.21g	$$⊢G\in \mathrm{V}\to \left(\underset{\dot{}}{[}G/f\underset{\dot{}}{]}\left(i\in \mathrm{\omega }\to \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)\right)\leftrightarrow \left(i\in \mathrm{\omega }\to \underset{\dot{}}{[}G/f\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)\right)\right)$$
9	3 8	ax-mp	$$⊢\underset{\dot{}}{[}G/f\underset{\dot{}}{]}\left(i\in \mathrm{\omega }\to \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)\right)\leftrightarrow \left(i\in \mathrm{\omega }\to \underset{\dot{}}{[}G/f\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)\right)$$
10		nfv	$$⊢Ⅎf\mathrm{suc}i\in N$$
11	10	sbc19.21g	$$⊢G\in \mathrm{V}\to \left(\underset{\dot{}}{[}G/f\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 N\to \underset{\dot{}}{[}G/f\underset{\dot{}}{]}f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
12	3 11	ax-mp	$$⊢\underset{\dot{}}{[}G/f\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 N\to \underset{\dot{}}{[}G/f\underset{\dot{}}{]}f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
13		fveq1	$$⊢f=G\to f\left(\mathrm{suc}i\right)=G\left(\mathrm{suc}i\right)$$
14		fveq1	$$⊢f=G\to f\left(i\right)=G\left(i\right)$$
15	14	bnj1113	$$⊢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)$$
16	13 15	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)$$
17		fveq1	$$⊢f=e\to f\left(\mathrm{suc}i\right)=e\left(\mathrm{suc}i\right)$$
18		fveq1	$$⊢f=e\to f\left(i\right)=e\left(i\right)$$
19	18	bnj1113	$$⊢f=e\to \bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)=\bigcup _{y\in e\left(i\right)}pred\left(y,A,R\right)$$
20	17 19	eqeq12d	$$⊢f=e\to \left(f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\leftrightarrow e\left(\mathrm{suc}i\right)=\bigcup _{y\in e\left(i\right)}pred\left(y,A,R\right)\right)$$
21		fveq1	$$⊢e=G\to e\left(\mathrm{suc}i\right)=G\left(\mathrm{suc}i\right)$$
22		fveq1	$$⊢e=G\to e\left(i\right)=G\left(i\right)$$
23	22	bnj1113	$$⊢e=G\to \bigcup _{y\in e\left(i\right)}pred\left(y,A,R\right)=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)$$
24	21 23	eqeq12d	$$⊢e=G\to \left(e\left(\mathrm{suc}i\right)=\bigcup _{y\in e\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)$$
25	3 16 20 24	bnj610	$$⊢\underset{\dot{}}{[}G/f\underset{\dot{}}{]}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)$$
26	25	imbi2i	$$⊢\left(\mathrm{suc}i\in N\to \underset{\dot{}}{[}G/f\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 N\to G\left(\mathrm{suc}i\right)=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)\right)$$
27	12 26	bitri	$$⊢\underset{\dot{}}{[}G/f\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 N\to G\left(\mathrm{suc}i\right)=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)\right)$$
28	27	imbi2i	$$⊢\left(i\in \mathrm{\omega }\to \underset{\dot{}}{[}G/f\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)\right)\leftrightarrow \left(i\in \mathrm{\omega }\to \left(\mathrm{suc}i\in N\to G\left(\mathrm{suc}i\right)=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
29	9 28	bitri	$$⊢\underset{\dot{}}{[}G/f\underset{\dot{}}{]}\left(i\in \mathrm{\omega }\to \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)\right)\leftrightarrow \left(i\in \mathrm{\omega }\to \left(\mathrm{suc}i\in N\to G\left(\mathrm{suc}i\right)=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
30	29	albii	$$⊢\forall i\underset{\dot{}}{[}G/f\underset{\dot{}}{]}\left(i\in \mathrm{\omega }\to \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)\right)\leftrightarrow \forall i\left(i\in \mathrm{\omega }\to \left(\mathrm{suc}i\in N\to G\left(\mathrm{suc}i\right)=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
31		sbcal	$$⊢\underset{\dot{}}{[}G/f\underset{\dot{}}{]}\forall i\left(i\in \mathrm{\omega }\to \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)\right)\leftrightarrow \forall i\underset{\dot{}}{[}G/f\underset{\dot{}}{]}\left(i\in \mathrm{\omega }\to \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)\right)$$
32		df-ral	$$⊢\forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in N\to G\left(\mathrm{suc}i\right)=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)\right)\leftrightarrow \forall i\left(i\in \mathrm{\omega }\to \left(\mathrm{suc}i\in N\to G\left(\mathrm{suc}i\right)=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)\right)\right)$$
33	30 31 32	3bitr4ri	$$⊢\forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in N\to G\left(\mathrm{suc}i\right)=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)\right)\leftrightarrow \underset{\dot{}}{[}G/f\underset{\dot{}}{]}\forall i\left(i\in \mathrm{\omega }\to \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)\right)$$
34	1	sbcbii	$$⊢\underset{\dot{}}{[}G/f\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}G/f\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)$$
35	6 33 34	3bitr4ri	$$⊢\underset{\dot{}}{[}G/f\underset{\dot{}}{]}\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in N\to G\left(\mathrm{suc}i\right)=\bigcup _{y\in G\left(i\right)}pred\left(y,A,R\right)\right)$$
36	2 35	bitri	Could not format ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. N -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode |-