Theorem bnj601

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	bnj601.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
	bnj601.2	$$⊢\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)$$
	bnj601.3	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
	bnj601.4	$$⊢\chi \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
	bnj601.5	$$⊢\theta \leftrightarrow \forall m\in D\left(m\mathrm{E}n\to \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\chi \right)$$
Assertion	bnj601	$$⊢n\ne 1_{𝑜}\to \left(\left(n\in D\wedge \theta \right)\to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bnj601.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
2		bnj601.2	$$⊢\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)$$
3		bnj601.3	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
4		bnj601.4	$$⊢\chi \leftrightarrow \left(\left(RFrSeA\wedge x\in A\right)\to \exists !f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
5		bnj601.5	$$⊢\theta \leftrightarrow \forall m\in D\left(m\mathrm{E}n\to \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\chi \right)$$
6		biid	$$⊢\underset{\dot{}}{[}m/n\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\phi$$
7		biid	$$⊢\underset{\dot{}}{[}m/n\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\psi$$
8		biid	$$⊢\underset{\dot{}}{[}m/n\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\chi$$
9		bnj602	$$⊢y=z\to pred\left(y,A,R\right)=pred\left(z,A,R\right)$$
10	9	cbviunv	$$⊢\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)=\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)$$
11	10	opeq2i	$$⊢⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩=⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩$$
12	11	sneqi	$$⊢\left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}=\left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}$$
13	12	uneq2i	$$⊢f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}=f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}$$
14		dfsbcq	$$⊢f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}=f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\to \left(\underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\phi \right)$$
15	13 14	ax-mp	$$⊢\underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\phi$$
16		dfsbcq	$$⊢f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}=f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\to \left(\underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\psi \right)$$
17	13 16	ax-mp	$$⊢\underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\psi$$
18		dfsbcq	$$⊢f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}=f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\to \left(\underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\chi \right)$$
19	13 18	ax-mp	$$⊢\underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}\left(f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\right)/f\underset{\dot{}}{]}\chi$$
20	13	eqcomi	$$⊢f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}=f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}$$
21		biid	$$⊢\left(fFnm\wedge \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\psi \right)\leftrightarrow \left(fFnm\wedge \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\psi \right)$$
22		biid	$$⊢\left(m\in D\wedge n=\mathrm{suc}m\wedge p\in m\right)\leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in m\right)$$
23		biid	$$⊢\left(m\in D\wedge n=\mathrm{suc}m\wedge p\in \mathrm{\omega }\wedge m=\mathrm{suc}p\right)\leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in \mathrm{\omega }\wedge m=\mathrm{suc}p\right)$$
24		biid	$$⊢\left(i\in \mathrm{\omega }\wedge \mathrm{suc}i\in n\wedge m=\mathrm{suc}i\right)\leftrightarrow \left(i\in \mathrm{\omega }\wedge \mathrm{suc}i\in n\wedge m=\mathrm{suc}i\right)$$
25		biid	$$⊢\left(i\in \mathrm{\omega }\wedge \mathrm{suc}i\in n\wedge m\ne \mathrm{suc}i\right)\leftrightarrow \left(i\in \mathrm{\omega }\wedge \mathrm{suc}i\in n\wedge m\ne \mathrm{suc}i\right)$$
26		eqid	$$⊢\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)$$
27		eqid	$$⊢\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)=\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)$$
28		eqid	$$⊢\bigcup _{y\in \left(f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\right)\left(i\right)}pred\left(y,A,R\right)=\bigcup _{y\in \left(f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\right)\left(i\right)}pred\left(y,A,R\right)$$
29		eqid	$$⊢\bigcup _{y\in \left(f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\right)\left(p\right)}pred\left(y,A,R\right)=\bigcup _{y\in \left(f\cup \left\{⟨m,\bigcup _{z\in f\left(p\right)}pred\left(z,A,R\right)⟩\right\}\right)\left(p\right)}pred\left(y,A,R\right)$$
30	1 2 3 4 5 6 7 8 15 17 19 20 21 22 23 24 25 26 27 28 29 20	bnj600	$$⊢n\ne 1_{𝑜}\to \left(\left(n\in D\wedge \theta \right)\to \chi \right)$$