Theorem bnj605

Description: Technical lemma. 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	bnj605.5	$$⊢\theta \leftrightarrow \forall m\in D\left(m\mathrm{E}n\to \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\chi \right)$$
	bnj605.13	No typesetting found for |- ( ph" <-> [. f / f ]. ph ) with typecode |-
	bnj605.14	No typesetting found for |- ( ps" <-> [. f / f ]. ps ) with typecode |-
	bnj605.17	No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
	bnj605.19	$$⊢\eta \leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in \mathrm{\omega }\wedge m=\mathrm{suc}p\right)$$
	bnj605.28	$$⊢f\in \mathrm{V}$$
	bnj605.31	No typesetting found for |- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode |-
	bnj605.32	No typesetting found for |- ( ph" <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
	bnj605.33	No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
	bnj605.37	$$⊢\left(n\ne 1_{𝑜}\wedge n\in D\right)\to \exists m\exists p\eta$$
	bnj605.38	No typesetting found for |- ( ( th /\ m e. D /\ m _E n ) -> ch' ) with typecode |-
	bnj605.41	$$⊢\left(RFrSeA\wedge \tau \wedge \eta \right)\to fFnn$$
	bnj605.42	No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode |-
	bnj605.43	No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode |-
Assertion	bnj605	$$⊢\left(n\ne 1_{𝑜}\wedge n\in D\wedge \theta \right)\to \left(\left(RFrSeA\wedge x\in A\right)\to \exists f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		bnj605.5	$$⊢\theta \leftrightarrow \forall m\in D\left(m\mathrm{E}n\to \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\chi \right)$$
2		bnj605.13	Could not format ( ph" <-> [. f / f ]. ph ) : No typesetting found for |- ( ph" <-> [. f / f ]. ph ) with typecode |-
3		bnj605.14	Could not format ( ps" <-> [. f / f ]. ps ) : No typesetting found for |- ( ps" <-> [. f / f ]. ps ) with typecode |-
4		bnj605.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
5		bnj605.19	$$⊢\eta \leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in \mathrm{\omega }\wedge m=\mathrm{suc}p\right)$$
6		bnj605.28	$$⊢f\in \mathrm{V}$$
7		bnj605.31	Could not format ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) : No typesetting found for |- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode |-
8		bnj605.32	Could not format ( ph" <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph" <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
9		bnj605.33	Could not format ( ps" <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps" <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
10		bnj605.37	$$⊢\left(n\ne 1_{𝑜}\wedge n\in D\right)\to \exists m\exists p\eta$$
11		bnj605.38	Could not format ( ( th /\ m e. D /\ m _E n ) -> ch' ) : No typesetting found for |- ( ( th /\ m e. D /\ m _E n ) -> ch' ) with typecode |-
12		bnj605.41	$$⊢\left(RFrSeA\wedge \tau \wedge \eta \right)\to fFnn$$
13		bnj605.42	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ph" ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode |-
14		bnj605.43	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ps" ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode |-
15	10	anim1i	$$⊢\left(\left(n\ne 1_{𝑜}\wedge n\in D\right)\wedge \theta \right)\to \left(\exists m\exists p\eta \wedge \theta \right)$$
16		nfv	$$⊢Ⅎp\theta$$
17	16	19.41	$$⊢\exists p\left(\eta \wedge \theta \right)\leftrightarrow \left(\exists p\eta \wedge \theta \right)$$
18	17	exbii	$$⊢\exists m\exists p\left(\eta \wedge \theta \right)\leftrightarrow \exists m\left(\exists p\eta \wedge \theta \right)$$
19	1	bnj1095	$$⊢\theta \to \forall m\theta$$
20	19	nf5i	$$⊢Ⅎm\theta$$
21	20	19.41	$$⊢\exists m\left(\exists p\eta \wedge \theta \right)\leftrightarrow \left(\exists m\exists p\eta \wedge \theta \right)$$
22	18 21	bitr2i	$$⊢\left(\exists m\exists p\eta \wedge \theta \right)\leftrightarrow \exists m\exists p\left(\eta \wedge \theta \right)$$
23	15 22	sylib	$$⊢\left(\left(n\ne 1_{𝑜}\wedge n\in D\right)\wedge \theta \right)\to \exists m\exists p\left(\eta \wedge \theta \right)$$
24	5	bnj1232	$$⊢\eta \to m\in D$$
25		bnj219	$$⊢n=\mathrm{suc}m\to m\mathrm{E}n$$
26	5 25	bnj770	$$⊢\eta \to m\mathrm{E}n$$
27	24 26	jca	$$⊢\eta \to \left(m\in D\wedge m\mathrm{E}n\right)$$
28	27	anim1i	$$⊢\left(\eta \wedge \theta \right)\to \left(\left(m\in D\wedge m\mathrm{E}n\right)\wedge \theta \right)$$
29		bnj170	$$⊢\left(\theta \wedge m\in D\wedge m\mathrm{E}n\right)\leftrightarrow \left(\left(m\in D\wedge m\mathrm{E}n\right)\wedge \theta \right)$$
30	28 29	sylibr	$$⊢\left(\eta \wedge \theta \right)\to \left(\theta \wedge m\in D\wedge m\mathrm{E}n\right)$$
31	30 11	syl	Could not format ( ( et /\ th ) -> ch' ) : No typesetting found for |- ( ( et /\ th ) -> ch' ) with typecode |-
32		simpl	$$⊢\left(\eta \wedge \theta \right)\to \eta$$
33	31 32	jca	Could not format ( ( et /\ th ) -> ( ch' /\ et ) ) : No typesetting found for |- ( ( et /\ th ) -> ( ch' /\ et ) ) with typecode |-
34	33	2eximi	Could not format ( E. m E. p ( et /\ th ) -> E. m E. p ( ch' /\ et ) ) : No typesetting found for |- ( E. m E. p ( et /\ th ) -> E. m E. p ( ch' /\ et ) ) with typecode |-
35		bnj248	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) ) with typecode |-
36		pm3.35	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
37	7 36	sylan2b	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
38		euex	Could not format ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
39	37 38	syl	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
40	39 4	bnj1198	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ta ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ta ) with typecode |-
41	35 40	bnj832	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ta ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ta ) with typecode |-
42	12 13 14	3jca	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ( f Fn n /\ ph" /\ ps" ) ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ( f Fn n /\ ph" /\ ps" ) ) with typecode |-
43	42	3com23	Could not format ( ( R _FrSe A /\ et /\ ta ) -> ( f Fn n /\ ph" /\ ps" ) ) : No typesetting found for |- ( ( R _FrSe A /\ et /\ ta ) -> ( f Fn n /\ ph" /\ ps" ) ) with typecode |-
44	43	3expia	Could not format ( ( R _FrSe A /\ et ) -> ( ta -> ( f Fn n /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ et ) -> ( ta -> ( f Fn n /\ ph" /\ ps" ) ) ) with typecode |-
45	44	eximdv	Could not format ( ( R _FrSe A /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) with typecode |-
46	45	ad4ant14	Could not format ( ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) with typecode |-
47	35 46	sylbi	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) ) with typecode |-
48	41 47	mpd	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( f Fn n /\ ph" /\ ps" ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( f Fn n /\ ph" /\ ps" ) ) with typecode |-
49		bnj432	Could not format ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ch' /\ et ) /\ ( R _FrSe A /\ x e. A ) ) ) : No typesetting found for |- ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ch' /\ et ) /\ ( R _FrSe A /\ x e. A ) ) ) with typecode |-
50		biid	$$⊢fFnn\leftrightarrow fFnn$$
51		sbcid	$$⊢\underset{\dot{}}{[}f/f\underset{\dot{}}{]}\phi \leftrightarrow \phi$$
52	2 51	bitri	Could not format ( ph" <-> ph ) : No typesetting found for |- ( ph" <-> ph ) with typecode |-
53		sbcid	$$⊢\underset{\dot{}}{[}f/f\underset{\dot{}}{]}\psi \leftrightarrow \psi$$
54	3 53	bitri	Could not format ( ps" <-> ps ) : No typesetting found for |- ( ps" <-> ps ) with typecode |-
55	50 52 54	3anbi123i	Could not format ( ( f Fn n /\ ph" /\ ps" ) <-> ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( ( f Fn n /\ ph" /\ ps" ) <-> ( f Fn n /\ ph /\ ps ) ) with typecode |-
56	55	exbii	Could not format ( E. f ( f Fn n /\ ph" /\ ps" ) <-> E. f ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( E. f ( f Fn n /\ ph" /\ ps" ) <-> E. f ( f Fn n /\ ph /\ ps ) ) with typecode |-
57	48 49 56	3imtr3i	Could not format ( ( ( ch' /\ et ) /\ ( R _FrSe A /\ x e. A ) ) -> E. f ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( ( ( ch' /\ et ) /\ ( R _FrSe A /\ x e. A ) ) -> E. f ( f Fn n /\ ph /\ ps ) ) with typecode |-
58	57	ex	Could not format ( ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for |- ( ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) ) with typecode |-
59	58	exlimivv	Could not format ( E. m E. p ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) ) : No typesetting found for |- ( E. m E. p ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) ) with typecode |-
60	23 34 59	3syl	$$⊢\left(\left(n\ne 1_{𝑜}\wedge n\in D\right)\wedge \theta \right)\to \left(\left(RFrSeA\wedge x\in A\right)\to \exists f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$
61	60	3impa	$$⊢\left(n\ne 1_{𝑜}\wedge n\in D\wedge \theta \right)\to \left(\left(RFrSeA\wedge x\in A\right)\to \exists f\left(fFnn\wedge \phi \wedge \psi \right)\right)$$