Theorem bnj580

Description: Technical lemma for bnj579 . 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	bnj580.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
	bnj580.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)$$
	bnj580.3	$$⊢\chi \leftrightarrow \left(fFnn\wedge \phi \wedge \psi \right)$$
	bnj580.4	No typesetting found for |- ( ph' <-> [. g / f ]. ph ) with typecode |-
	bnj580.5	No typesetting found for |- ( ps' <-> [. g / f ]. ps ) with typecode |-
	bnj580.6	No typesetting found for |- ( ch' <-> [. g / f ]. ch ) with typecode |-
	bnj580.7	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
	bnj580.8	No typesetting found for |- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
	bnj580.9	$$⊢\tau \leftrightarrow \forall k\in n\left(k\mathrm{E}j\to \underset{\dot{}}{[}k/j\underset{\dot{}}{]}\theta \right)$$
Assertion	bnj580	$$⊢n\in D\to {\exists }^{*}f\chi$$

Proof

Step	Hyp	Ref	Expression
1		bnj580.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
2		bnj580.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		bnj580.3	$$⊢\chi \leftrightarrow \left(fFnn\wedge \phi \wedge \psi \right)$$
4		bnj580.4	Could not format ( ph' <-> [. g / f ]. ph ) : No typesetting found for |- ( ph' <-> [. g / f ]. ph ) with typecode |-
5		bnj580.5	Could not format ( ps' <-> [. g / f ]. ps ) : No typesetting found for |- ( ps' <-> [. g / f ]. ps ) with typecode |-
6		bnj580.6	Could not format ( ch' <-> [. g / f ]. ch ) : No typesetting found for |- ( ch' <-> [. g / f ]. ch ) with typecode |-
7		bnj580.7	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
8		bnj580.8	Could not format ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
9		bnj580.9	$$⊢\tau \leftrightarrow \forall k\in n\left(k\mathrm{E}j\to \underset{\dot{}}{[}k/j\underset{\dot{}}{]}\theta \right)$$
10	3	simp1bi	$$⊢\chi \to fFnn$$
11	3 4 5 6	bnj581	Could not format ( ch' <-> ( g Fn n /\ ph' /\ ps' ) ) : No typesetting found for |- ( ch' <-> ( g Fn n /\ ph' /\ ps' ) ) with typecode |-
12	11	simp1bi	Could not format ( ch' -> g Fn n ) : No typesetting found for |- ( ch' -> g Fn n ) with typecode |-
13	10 12	bnj240	Could not format ( ( n e. D /\ ch /\ ch' ) -> ( f Fn n /\ g Fn n ) ) : No typesetting found for |- ( ( n e. D /\ ch /\ ch' ) -> ( f Fn n /\ g Fn n ) ) with typecode |-
14	4 1	bnj154	Could not format ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( g ` (/) ) = _pred ( x , A , R ) ) with typecode |-
15		vex	$$⊢g\in \mathrm{V}$$
16	2 5 15	bnj540	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 |-
17	8	bnj591	Could not format ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) : No typesetting found for |- ( [. k / j ]. th <-> ( ( n e. D /\ ch /\ ch' ) -> ( f ` k ) = ( g ` k ) ) ) with typecode |-
18	1 2 3 7 14 16 11 8 17 9	bnj594	$$⊢\left(j\in n\wedge \tau \right)\to \theta$$
19	18	ex	$$⊢j\in n\to \left(\tau \to \theta \right)$$
20	19	rgen	$$⊢\forall j\in n\left(\tau \to \theta \right)$$
21		vex	$$⊢n\in \mathrm{V}$$
22	21 9	bnj110	$$⊢\left(\mathrm{E}\mathrm{Fr}n\wedge \forall j\in n\left(\tau \to \theta \right)\right)\to \forall j\in n\theta$$
23	20 22	mpan2	$$⊢\mathrm{E}\mathrm{Fr}n\to \forall j\in n\theta$$
24	8	ralbii	Could not format ( A. j e. n th <-> A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( A. j e. n th <-> A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
25	23 24	sylib	Could not format ( _E Fr n -> A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( _E Fr n -> A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
26	25	r19.21be	Could not format A. j e. n ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- A. j e. n ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
27	7	bnj923	$$⊢n\in D\to n\in \mathrm{\omega }$$
28		nnord	$$⊢n\in \mathrm{\omega }\to \mathrm{Ord}n$$
29		ordfr	$$⊢\mathrm{Ord}n\to \mathrm{E}\mathrm{Fr}n$$
30	27 28 29	3syl	$$⊢n\in D\to \mathrm{E}\mathrm{Fr}n$$
31	30	3ad2ant1	Could not format ( ( n e. D /\ ch /\ ch' ) -> _E Fr n ) : No typesetting found for |- ( ( n e. D /\ ch /\ ch' ) -> _E Fr n ) with typecode |-
32	31	pm4.71ri	Could not format ( ( n e. D /\ ch /\ ch' ) <-> ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) ) : No typesetting found for |- ( ( n e. D /\ ch /\ ch' ) <-> ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) ) with typecode |-
33	32	imbi1i	Could not format ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) ) with typecode |-
34		impexp	Could not format ( ( ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) <-> ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) : No typesetting found for |- ( ( ( _E Fr n /\ ( n e. D /\ ch /\ ch' ) ) -> ( f ` j ) = ( g ` j ) ) <-> ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) with typecode |-
35	33 34	bitri	Could not format ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) : No typesetting found for |- ( ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) with typecode |-
36	35	ralbii	Could not format ( A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> A. j e. n ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) : No typesetting found for |- ( A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> A. j e. n ( _E Fr n -> ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) ) ) with typecode |-
37	26 36	mpbir	Could not format A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) : No typesetting found for |- A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) with typecode |-
38		r19.21v	Could not format ( A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> A. j e. n ( f ` j ) = ( g ` j ) ) ) : No typesetting found for |- ( A. j e. n ( ( n e. D /\ ch /\ ch' ) -> ( f ` j ) = ( g ` j ) ) <-> ( ( n e. D /\ ch /\ ch' ) -> A. j e. n ( f ` j ) = ( g ` j ) ) ) with typecode |-
39	37 38	mpbi	Could not format ( ( n e. D /\ ch /\ ch' ) -> A. j e. n ( f ` j ) = ( g ` j ) ) : No typesetting found for |- ( ( n e. D /\ ch /\ ch' ) -> A. j e. n ( f ` j ) = ( g ` j ) ) with typecode |-
40		eqfnfv	$$⊢\left(fFnn\wedge gFnn\right)\to \left(f=g\leftrightarrow \forall j\in nf\left(j\right)=g\left(j\right)\right)$$
41	40	biimprd	$$⊢\left(fFnn\wedge gFnn\right)\to \left(\forall j\in nf\left(j\right)=g\left(j\right)\to f=g\right)$$
42	13 39 41	sylc	Could not format ( ( n e. D /\ ch /\ ch' ) -> f = g ) : No typesetting found for |- ( ( n e. D /\ ch /\ ch' ) -> f = g ) with typecode |-
43	42	3expib	Could not format ( n e. D -> ( ( ch /\ ch' ) -> f = g ) ) : No typesetting found for |- ( n e. D -> ( ( ch /\ ch' ) -> f = g ) ) with typecode |-
44	43	alrimivv	Could not format ( n e. D -> A. f A. g ( ( ch /\ ch' ) -> f = g ) ) : No typesetting found for |- ( n e. D -> A. f A. g ( ( ch /\ ch' ) -> f = g ) ) with typecode |-
45		sbsbc	$$⊢\left[g/f\right]\chi \leftrightarrow \underset{\dot{}}{[}g/f\underset{\dot{}}{]}\chi$$
46	45	anbi2i	$$⊢\left(\chi \wedge \left[g/f\right]\chi \right)\leftrightarrow \left(\chi \wedge \underset{\dot{}}{[}g/f\underset{\dot{}}{]}\chi \right)$$
47	46	imbi1i	$$⊢\left(\left(\chi \wedge \left[g/f\right]\chi \right)\to f=g\right)\leftrightarrow \left(\left(\chi \wedge \underset{\dot{}}{[}g/f\underset{\dot{}}{]}\chi \right)\to f=g\right)$$
48	47	2albii	$$⊢\forall f\forall g\left(\left(\chi \wedge \left[g/f\right]\chi \right)\to f=g\right)\leftrightarrow \forall f\forall g\left(\left(\chi \wedge \underset{\dot{}}{[}g/f\underset{\dot{}}{]}\chi \right)\to f=g\right)$$
49		nfv	$$⊢Ⅎg\chi$$
50	49	mo3	$$⊢{\exists }^{*}f\chi \leftrightarrow \forall f\forall g\left(\left(\chi \wedge \left[g/f\right]\chi \right)\to f=g\right)$$
51	6	anbi2i	Could not format ( ( ch /\ ch' ) <-> ( ch /\ [. g / f ]. ch ) ) : No typesetting found for |- ( ( ch /\ ch' ) <-> ( ch /\ [. g / f ]. ch ) ) with typecode |-
52	51	imbi1i	Could not format ( ( ( ch /\ ch' ) -> f = g ) <-> ( ( ch /\ [. g / f ]. ch ) -> f = g ) ) : No typesetting found for |- ( ( ( ch /\ ch' ) -> f = g ) <-> ( ( ch /\ [. g / f ]. ch ) -> f = g ) ) with typecode |-
53	52	2albii	Could not format ( A. f A. g ( ( ch /\ ch' ) -> f = g ) <-> A. f A. g ( ( ch /\ [. g / f ]. ch ) -> f = g ) ) : No typesetting found for |- ( A. f A. g ( ( ch /\ ch' ) -> f = g ) <-> A. f A. g ( ( ch /\ [. g / f ]. ch ) -> f = g ) ) with typecode |-
54	48 50 53	3bitr4i	Could not format ( E* f ch <-> A. f A. g ( ( ch /\ ch' ) -> f = g ) ) : No typesetting found for |- ( E* f ch <-> A. f A. g ( ( ch /\ ch' ) -> f = g ) ) with typecode |-
55	44 54	sylibr	$$⊢n\in D\to {\exists }^{*}f\chi$$