Theorem bnj543

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	bnj543.1	No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
	bnj543.2	No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
	bnj543.3	$$⊢G=f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}$$
	bnj543.4	No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
	bnj543.5	$$⊢\sigma \leftrightarrow \left(m\in \mathrm{\omega }\wedge n=\mathrm{suc}m\wedge p\in m\right)$$
Assertion	bnj543	$$⊢\left(RFrSeA\wedge \tau \wedge \sigma \right)\to GFnn$$

Proof

Step	Hyp	Ref	Expression
1		bnj543.1	Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
2		bnj543.2	Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
3		bnj543.3	$$⊢G=f\cup \left\{⟨m,\bigcup _{y\in f\left(p\right)}pred\left(y,A,R\right)⟩\right\}$$
4		bnj543.4	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
5		bnj543.5	$$⊢\sigma \leftrightarrow \left(m\in \mathrm{\omega }\wedge n=\mathrm{suc}m\wedge p\in m\right)$$
6		bnj257	Could not format ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ f Fn m /\ n = suc m ) ) : No typesetting found for |- ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ f Fn m /\ n = suc m ) ) with typecode |-
7		bnj268	Could not format ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ f Fn m /\ n = suc m ) <-> ( ( ph' /\ ps' ) /\ f Fn m /\ ( m e. _om /\ p e. m ) /\ n = suc m ) ) : No typesetting found for |- ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ f Fn m /\ n = suc m ) <-> ( ( ph' /\ ps' ) /\ f Fn m /\ ( m e. _om /\ p e. m ) /\ n = suc m ) ) with typecode |-
8	6 7	bitri	Could not format ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ph' /\ ps' ) /\ f Fn m /\ ( m e. _om /\ p e. m ) /\ n = suc m ) ) : No typesetting found for |- ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ph' /\ ps' ) /\ f Fn m /\ ( m e. _om /\ p e. m ) /\ n = suc m ) ) with typecode |-
9		bnj253	Could not format ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) /\ n = suc m /\ f Fn m ) ) : No typesetting found for |- ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) /\ n = suc m /\ f Fn m ) ) with typecode |-
10		bnj256	Could not format ( ( ( ph' /\ ps' ) /\ f Fn m /\ ( m e. _om /\ p e. m ) /\ n = suc m ) <-> ( ( ( ph' /\ ps' ) /\ f Fn m ) /\ ( ( m e. _om /\ p e. m ) /\ n = suc m ) ) ) : No typesetting found for |- ( ( ( ph' /\ ps' ) /\ f Fn m /\ ( m e. _om /\ p e. m ) /\ n = suc m ) <-> ( ( ( ph' /\ ps' ) /\ f Fn m ) /\ ( ( m e. _om /\ p e. m ) /\ n = suc m ) ) ) with typecode |-
11	8 9 10	3bitr3i	Could not format ( ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) /\ n = suc m /\ f Fn m ) <-> ( ( ( ph' /\ ps' ) /\ f Fn m ) /\ ( ( m e. _om /\ p e. m ) /\ n = suc m ) ) ) : No typesetting found for |- ( ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) /\ n = suc m /\ f Fn m ) <-> ( ( ( ph' /\ ps' ) /\ f Fn m ) /\ ( ( m e. _om /\ p e. m ) /\ n = suc m ) ) ) with typecode |-
12		bnj256	Could not format ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) ) : No typesetting found for |- ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) ) with typecode |-
13	12	3anbi1i	Could not format ( ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) /\ n = suc m /\ f Fn m ) ) : No typesetting found for |- ( ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ( ph' /\ ps' ) /\ ( m e. _om /\ p e. m ) ) /\ n = suc m /\ f Fn m ) ) with typecode |-
14		bnj170	Could not format ( ( f Fn m /\ ph' /\ ps' ) <-> ( ( ph' /\ ps' ) /\ f Fn m ) ) : No typesetting found for |- ( ( f Fn m /\ ph' /\ ps' ) <-> ( ( ph' /\ ps' ) /\ f Fn m ) ) with typecode |-
15	4 14	bitri	Could not format ( ta <-> ( ( ph' /\ ps' ) /\ f Fn m ) ) : No typesetting found for |- ( ta <-> ( ( ph' /\ ps' ) /\ f Fn m ) ) with typecode |-
16		3anan32	$$⊢\left(m\in \mathrm{\omega }\wedge n=\mathrm{suc}m\wedge p\in m\right)\leftrightarrow \left(\left(m\in \mathrm{\omega }\wedge p\in m\right)\wedge n=\mathrm{suc}m\right)$$
17	5 16	bitri	$$⊢\sigma \leftrightarrow \left(\left(m\in \mathrm{\omega }\wedge p\in m\right)\wedge n=\mathrm{suc}m\right)$$
18	15 17	anbi12i	Could not format ( ( ta /\ si ) <-> ( ( ( ph' /\ ps' ) /\ f Fn m ) /\ ( ( m e. _om /\ p e. m ) /\ n = suc m ) ) ) : No typesetting found for |- ( ( ta /\ si ) <-> ( ( ( ph' /\ ps' ) /\ f Fn m ) /\ ( ( m e. _om /\ p e. m ) /\ n = suc m ) ) ) with typecode |-
19	11 13 18	3bitr4ri	Could not format ( ( ta /\ si ) <-> ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) : No typesetting found for |- ( ( ta /\ si ) <-> ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) with typecode |-
20	19	anbi2i	Could not format ( ( R _FrSe A /\ ( ta /\ si ) ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ ( ta /\ si ) ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) ) with typecode |-
21		3anass	$$⊢\left(RFrSeA\wedge \tau \wedge \sigma \right)\leftrightarrow \left(RFrSeA\wedge \left(\tau \wedge \sigma \right)\right)$$
22		bnj252	Could not format ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) ) with typecode |-
23	20 21 22	3bitr4i	Could not format ( ( R _FrSe A /\ ta /\ si ) <-> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ si ) <-> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) with typecode |-
24		df-suc	$$⊢\mathrm{suc}m=m\cup \left\{m\right\}$$
25	24	eqeq2i	$$⊢n=\mathrm{suc}m\leftrightarrow n=m\cup \left\{m\right\}$$
26	25	3anbi2i	Could not format ( ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) ) : No typesetting found for |- ( ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) ) with typecode |-
27	26	anbi2i	Could not format ( ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) ) ) with typecode |-
28		bnj252	Could not format ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) <-> ( R _FrSe A /\ ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) ) ) with typecode |-
29	27 22 28	3bitr4i	Could not format ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) ) : No typesetting found for |- ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) <-> ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) ) with typecode |-
30		biid	Could not format ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) : No typesetting found for |- ( ( ph' /\ ps' /\ m e. _om /\ p e. m ) <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) with typecode |-
31	1 2 3 30	bnj535	Could not format ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) -> G Fn n ) : No typesetting found for |- ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = ( m u. { m } ) /\ f Fn m ) -> G Fn n ) with typecode |-
32	29 31	sylbi	Could not format ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) -> G Fn n ) : No typesetting found for |- ( ( R _FrSe A /\ ( ph' /\ ps' /\ m e. _om /\ p e. m ) /\ n = suc m /\ f Fn m ) -> G Fn n ) with typecode |-
33	23 32	sylbi	$$⊢\left(RFrSeA\wedge \tau \wedge \sigma \right)\to GFnn$$