Theorem bnj1000

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	bnj1000.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)$$
	bnj1000.2	No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
	bnj1000.3	$$⊢G\in \mathrm{V}$$
	bnj1000.15	$$⊢C=\bigcup _{y\in f\left(m\right)}pred\left(y,A,R\right)$$
	bnj1000.16	$$⊢G=f\cup \left\{⟨n,C⟩\right\}$$
Assertion	bnj1000	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		bnj1000.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		bnj1000.2	Could not format ( ps" <-> [. G / f ]. ps ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
3		bnj1000.3	$$⊢G\in \mathrm{V}$$
4		bnj1000.15	$$⊢C=\bigcup _{y\in f\left(m\right)}pred\left(y,A,R\right)$$
5		bnj1000.16	$$⊢G=f\cup \left\{⟨n,C⟩\right\}$$
6		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)$$
7	6	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)$$
8	7	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)$$
9		nfv	$$⊢Ⅎfi\in \mathrm{\omega }$$
10	9	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)$$
11	3 10	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)$$
12		nfv	$$⊢Ⅎf\mathrm{suc}i\in N$$
13	12	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)$$
14	3 13	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)$$
15		fveq1	$$⊢f=G\to f\left(\mathrm{suc}i\right)=G\left(\mathrm{suc}i\right)$$
16		fveq1	$$⊢f=G\to f\left(i\right)=G\left(i\right)$$
17		ax-5	$$⊢w\in f\left(i\right)\to \forall yw\in f\left(i\right)$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}yf$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}yn$$
20		nfiu1	$$⊢\underset{\_}{Ⅎ}y\bigcup _{y\in f\left(m\right)}pred\left(y,A,R\right)$$
21	4 20	nfcxfr	$$⊢\underset{\_}{Ⅎ}yC$$
22	19 21	nfop	$$⊢\underset{\_}{Ⅎ}y⟨n,C⟩$$
23	22	nfsn	$$⊢\underset{\_}{Ⅎ}y\left\{⟨n,C⟩\right\}$$
24	18 23	nfun	$$⊢\underset{\_}{Ⅎ}y\left(f\cup \left\{⟨n,C⟩\right\}\right)$$
25	5 24	nfcxfr	$$⊢\underset{\_}{Ⅎ}yG$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}yi$$
27	25 26	nffv	$$⊢\underset{\_}{Ⅎ}yG\left(i\right)$$
28	27	nfcrii	$$⊢w\in G\left(i\right)\to \forall yw\in G\left(i\right)$$
29	17 28	bnj1316	$$⊢f\left(i\right)=G\left(i\right)\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)$$
30	16 29	syl	$$⊢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)$$
31	15 30	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)$$
32		fveq1	$$⊢f=e\to f\left(\mathrm{suc}i\right)=e\left(\mathrm{suc}i\right)$$
33		fveq1	$$⊢f=e\to f\left(i\right)=e\left(i\right)$$
34		ax-5	$$⊢f\left(i\right)=e\left(i\right)\to \forall yf\left(i\right)=e\left(i\right)$$
35	34	bnj956	$$⊢f\left(i\right)=e\left(i\right)\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)$$
36	33 35	syl	$$⊢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)$$
37	32 36	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)$$
38		fveq1	$$⊢e=G\to e\left(\mathrm{suc}i\right)=G\left(\mathrm{suc}i\right)$$
39		fveq1	$$⊢e=G\to e\left(i\right)=G\left(i\right)$$
40		ax-5	$$⊢w\in e\left(i\right)\to \forall yw\in e\left(i\right)$$
41	40 28	bnj1316	$$⊢e\left(i\right)=G\left(i\right)\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)$$
42	39 41	syl	$$⊢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)$$
43	38 42	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)$$
44	3 31 37 43	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)$$
45	44	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)$$
46	14 45	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)$$
47	46	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)$$
48	11 47	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)$$
49	48	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)$$
50		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)$$
51		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)$$
52	49 50 51	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)$$
53	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)$$
54	8 52 53	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)$$
55	2 54	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 |-