Theorem bnj607

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	bnj607.5	$$⊢\theta \leftrightarrow \forall m\in D\left(m\mathrm{E}n\to \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\chi \right)$$
	bnj607.13	No typesetting found for |- ( ph" <-> [. G / f ]. ph ) with typecode |-
	bnj607.14	No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
	bnj607.17	No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
	bnj607.19	$$⊢\eta \leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in \mathrm{\omega }\wedge m=\mathrm{suc}p\right)$$
	bnj607.28	$$⊢G\in \mathrm{V}$$
	bnj607.31	No typesetting found for |- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) with typecode |-
	bnj607.32	No typesetting found for |- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode |-
	bnj607.33	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 |-
	bnj607.37	$$⊢\left(n\ne 1_{𝑜}\wedge n\in D\right)\to \exists m\exists p\eta$$
	bnj607.38	No typesetting found for |- ( ( th /\ m e. D /\ m _E n ) -> ch' ) with typecode |-
	bnj607.41	$$⊢\left(RFrSeA\wedge \tau \wedge \eta \right)\to GFnn$$
	bnj607.42	No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode |-
	bnj607.43	No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode |-
	bnj607.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
	bnj607.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)$$
	bnj607.400	No typesetting found for |- ( ph0 <-> [. h / f ]. ph ) with typecode |-
	bnj607.401	No typesetting found for |- ( ps0 <-> [. h / f ]. ps ) with typecode |-
	bnj607.300	No typesetting found for |- ( ph1 <-> [. G / h ]. ph0 ) with typecode |-
	bnj607.301	No typesetting found for |- ( ps1 <-> [. G / h ]. ps0 ) with typecode |-
Assertion	bnj607	$$⊢\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		bnj607.5	$$⊢\theta \leftrightarrow \forall m\in D\left(m\mathrm{E}n\to \underset{\dot{}}{[}m/n\underset{\dot{}}{]}\chi \right)$$
2		bnj607.13	Could not format ( ph" <-> [. G / f ]. ph ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph ) with typecode |-
3		bnj607.14	Could not format ( ps" <-> [. G / f ]. ps ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps ) with typecode |-
4		bnj607.17	Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
5		bnj607.19	$$⊢\eta \leftrightarrow \left(m\in D\wedge n=\mathrm{suc}m\wedge p\in \mathrm{\omega }\wedge m=\mathrm{suc}p\right)$$
6		bnj607.28	$$⊢G\in \mathrm{V}$$
7		bnj607.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		bnj607.32	Could not format ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode |-
9		bnj607.33	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 |-
10		bnj607.37	$$⊢\left(n\ne 1_{𝑜}\wedge n\in D\right)\to \exists m\exists p\eta$$
11		bnj607.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		bnj607.41	$$⊢\left(RFrSeA\wedge \tau \wedge \eta \right)\to GFnn$$
13		bnj607.42	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ph" ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ph" ) with typecode |-
14		bnj607.43	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ps" ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ps" ) with typecode |-
15		bnj607.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(x,A,R\right)$$
16		bnj607.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)$$
17		bnj607.400	Could not format ( ph0 <-> [. h / f ]. ph ) : No typesetting found for |- ( ph0 <-> [. h / f ]. ph ) with typecode |-
18		bnj607.401	Could not format ( ps0 <-> [. h / f ]. ps ) : No typesetting found for |- ( ps0 <-> [. h / f ]. ps ) with typecode |-
19		bnj607.300	Could not format ( ph1 <-> [. G / h ]. ph0 ) : No typesetting found for |- ( ph1 <-> [. G / h ]. ph0 ) with typecode |-
20		bnj607.301	Could not format ( ps1 <-> [. G / h ]. ps0 ) : No typesetting found for |- ( ps1 <-> [. G / h ]. ps0 ) with typecode |-
21	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)$$
22		nfv	$$⊢Ⅎp\theta$$
23	22	19.41	$$⊢\exists p\left(\eta \wedge \theta \right)\leftrightarrow \left(\exists p\eta \wedge \theta \right)$$
24	23	exbii	$$⊢\exists m\exists p\left(\eta \wedge \theta \right)\leftrightarrow \exists m\left(\exists p\eta \wedge \theta \right)$$
25	1	bnj1095	$$⊢\theta \to \forall m\theta$$
26	25	nf5i	$$⊢Ⅎm\theta$$
27	26	19.41	$$⊢\exists m\left(\exists p\eta \wedge \theta \right)\leftrightarrow \left(\exists m\exists p\eta \wedge \theta \right)$$
28	24 27	bitr2i	$$⊢\left(\exists m\exists p\eta \wedge \theta \right)\leftrightarrow \exists m\exists p\left(\eta \wedge \theta \right)$$
29	21 28	sylib	$$⊢\left(\left(n\ne 1_{𝑜}\wedge n\in D\right)\wedge \theta \right)\to \exists m\exists p\left(\eta \wedge \theta \right)$$
30	5	bnj1232	$$⊢\eta \to m\in D$$
31		bnj219	$$⊢n=\mathrm{suc}m\to m\mathrm{E}n$$
32	5 31	bnj770	$$⊢\eta \to m\mathrm{E}n$$
33	30 32	jca	$$⊢\eta \to \left(m\in D\wedge m\mathrm{E}n\right)$$
34	33	anim1i	$$⊢\left(\eta \wedge \theta \right)\to \left(\left(m\in D\wedge m\mathrm{E}n\right)\wedge \theta \right)$$
35		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)$$
36	34 35	sylibr	$$⊢\left(\eta \wedge \theta \right)\to \left(\theta \wedge m\in D\wedge m\mathrm{E}n\right)$$
37	36 11	syl	Could not format ( ( et /\ th ) -> ch' ) : No typesetting found for |- ( ( et /\ th ) -> ch' ) with typecode |-
38		simpl	$$⊢\left(\eta \wedge \theta \right)\to \eta$$
39	37 38	jca	Could not format ( ( et /\ th ) -> ( ch' /\ et ) ) : No typesetting found for |- ( ( et /\ th ) -> ( ch' /\ et ) ) with typecode |-
40	39	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 |-
41	7	biimpi	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 |-
42		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 |-
43	41 42	syl6	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 |-
44	43	impcom	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 |-
45	44 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 |-
46	45	adantrr	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 |-
47		id	$$⊢\left(RFrSeA\wedge \tau \wedge \eta \right)\to \left(RFrSeA\wedge \tau \wedge \eta \right)$$
48	47	3com23	$$⊢\left(RFrSeA\wedge \eta \wedge \tau \right)\to \left(RFrSeA\wedge \tau \wedge \eta \right)$$
49	48	3expia	$$⊢\left(RFrSeA\wedge \eta \right)\to \left(\tau \to \left(RFrSeA\wedge \tau \wedge \eta \right)\right)$$
50	49	eximdv	$$⊢\left(RFrSeA\wedge \eta \right)\to \left(\exists f\tau \to \exists f\left(RFrSeA\wedge \tau \wedge \eta \right)\right)$$
51	50	ad2ant2rl	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> ( E. f ta -> E. f ( R _FrSe A /\ ta /\ et ) ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> ( E. f ta -> E. f ( R _FrSe A /\ ta /\ et ) ) ) with typecode |-
52	46 51	mpd	Could not format ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ( R _FrSe A /\ ta /\ et ) ) : No typesetting found for |- ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ( R _FrSe A /\ ta /\ et ) ) with typecode |-
53	12 13 14	3jca	Could not format ( ( R _FrSe A /\ ta /\ et ) -> ( G Fn n /\ ph" /\ ps" ) ) : No typesetting found for |- ( ( R _FrSe A /\ ta /\ et ) -> ( G Fn n /\ ph" /\ ps" ) ) with typecode |-
54	53	eximi	Could not format ( E. f ( R _FrSe A /\ ta /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) ) : No typesetting found for |- ( E. f ( R _FrSe A /\ ta /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) ) with typecode |-
55		nfe1	$$⊢Ⅎf\exists f\left(fFnn\wedge \phi \wedge \psi \right)$$
56		nfcv	$$⊢\underset{\_}{Ⅎ}hG$$
57		nfv	$$⊢ℲhGFnn$$
58		nfsbc1v	Could not format F/ h [. G / h ]. ph0 : No typesetting found for |- F/ h [. G / h ]. ph0 with typecode |-
59	19 58	nfxfr	Could not format F/ h ph1 : No typesetting found for |- F/ h ph1 with typecode |-
60		nfsbc1v	Could not format F/ h [. G / h ]. ps0 : No typesetting found for |- F/ h [. G / h ]. ps0 with typecode |-
61	20 60	nfxfr	Could not format F/ h ps1 : No typesetting found for |- F/ h ps1 with typecode |-
62	57 59 61	nf3an	Could not format F/ h ( G Fn n /\ ph1 /\ ps1 ) : No typesetting found for |- F/ h ( G Fn n /\ ph1 /\ ps1 ) with typecode |-
63		fneq1	$$⊢h=G\to \left(hFnn\leftrightarrow GFnn\right)$$
64		sbceq1a	Could not format ( h = G -> ( ph0 <-> [. G / h ]. ph0 ) ) : No typesetting found for |- ( h = G -> ( ph0 <-> [. G / h ]. ph0 ) ) with typecode |-
65	64 19	bitr4di	Could not format ( h = G -> ( ph0 <-> ph1 ) ) : No typesetting found for |- ( h = G -> ( ph0 <-> ph1 ) ) with typecode |-
66		sbceq1a	Could not format ( h = G -> ( ps0 <-> [. G / h ]. ps0 ) ) : No typesetting found for |- ( h = G -> ( ps0 <-> [. G / h ]. ps0 ) ) with typecode |-
67	66 20	bitr4di	Could not format ( h = G -> ( ps0 <-> ps1 ) ) : No typesetting found for |- ( h = G -> ( ps0 <-> ps1 ) ) with typecode |-
68	63 65 67	3anbi123d	Could not format ( h = G -> ( ( h Fn n /\ ph0 /\ ps0 ) <-> ( G Fn n /\ ph1 /\ ps1 ) ) ) : No typesetting found for |- ( h = G -> ( ( h Fn n /\ ph0 /\ ps0 ) <-> ( G Fn n /\ ph1 /\ ps1 ) ) ) with typecode |-
69	56 62 68	spcegf	Could not format ( G e. _V -> ( ( G Fn n /\ ph1 /\ ps1 ) -> E. h ( h Fn n /\ ph0 /\ ps0 ) ) ) : No typesetting found for |- ( G e. _V -> ( ( G Fn n /\ ph1 /\ ps1 ) -> E. h ( h Fn n /\ ph0 /\ ps0 ) ) ) with typecode |-
70	6 69	ax-mp	Could not format ( ( G Fn n /\ ph1 /\ ps1 ) -> E. h ( h Fn n /\ ph0 /\ ps0 ) ) : No typesetting found for |- ( ( G Fn n /\ ph1 /\ ps1 ) -> E. h ( h Fn n /\ ph0 /\ ps0 ) ) with typecode |-
71	17 15	bnj154	Could not format ( ph0 <-> ( h ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph0 <-> ( h ` (/) ) = _pred ( x , A , R ) ) with typecode |-
72	71 19 6	bnj526	Could not format ( ph1 <-> ( G ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph1 <-> ( G ` (/) ) = _pred ( x , A , R ) ) with typecode |-
73	8 72	bitr4i	Could not format ( ph" <-> ph1 ) : No typesetting found for |- ( ph" <-> ph1 ) with typecode |-
74		vex	$$⊢h\in \mathrm{V}$$
75	16 18 74	bnj540	Could not format ( ps0 <-> A. i e. _om ( suc i e. n -> ( h ` suc i ) = U_ y e. ( h ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps0 <-> A. i e. _om ( suc i e. n -> ( h ` suc i ) = U_ y e. ( h ` i ) _pred ( y , A , R ) ) ) with typecode |-
76	75 20 6	bnj540	Could not format ( ps1 <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps1 <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) ) with typecode |-
77	9 76	bitr4i	Could not format ( ps" <-> ps1 ) : No typesetting found for |- ( ps" <-> ps1 ) with typecode |-
78	73 77	anbi12i	Could not format ( ( ph" /\ ps" ) <-> ( ph1 /\ ps1 ) ) : No typesetting found for |- ( ( ph" /\ ps" ) <-> ( ph1 /\ ps1 ) ) with typecode |-
79	78	anbi2i	Could not format ( ( G Fn n /\ ( ph" /\ ps" ) ) <-> ( G Fn n /\ ( ph1 /\ ps1 ) ) ) : No typesetting found for |- ( ( G Fn n /\ ( ph" /\ ps" ) ) <-> ( G Fn n /\ ( ph1 /\ ps1 ) ) ) with typecode |-
80		3anass	Could not format ( ( G Fn n /\ ph" /\ ps" ) <-> ( G Fn n /\ ( ph" /\ ps" ) ) ) : No typesetting found for |- ( ( G Fn n /\ ph" /\ ps" ) <-> ( G Fn n /\ ( ph" /\ ps" ) ) ) with typecode |-
81		3anass	Could not format ( ( G Fn n /\ ph1 /\ ps1 ) <-> ( G Fn n /\ ( ph1 /\ ps1 ) ) ) : No typesetting found for |- ( ( G Fn n /\ ph1 /\ ps1 ) <-> ( G Fn n /\ ( ph1 /\ ps1 ) ) ) with typecode |-
82	79 80 81	3bitr4i	Could not format ( ( G Fn n /\ ph" /\ ps" ) <-> ( G Fn n /\ ph1 /\ ps1 ) ) : No typesetting found for |- ( ( G Fn n /\ ph" /\ ps" ) <-> ( G Fn n /\ ph1 /\ ps1 ) ) with typecode |-
83		nfv	$$⊢Ⅎh\left(fFnn\wedge \phi \wedge \psi \right)$$
84		nfv	$$⊢ℲfhFnn$$
85		nfsbc1v	$$⊢Ⅎf\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi$$
86	17 85	nfxfr	Could not format F/ f ph0 : No typesetting found for |- F/ f ph0 with typecode |-
87		nfsbc1v	$$⊢Ⅎf\underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi$$
88	18 87	nfxfr	Could not format F/ f ps0 : No typesetting found for |- F/ f ps0 with typecode |-
89	84 86 88	nf3an	Could not format F/ f ( h Fn n /\ ph0 /\ ps0 ) : No typesetting found for |- F/ f ( h Fn n /\ ph0 /\ ps0 ) with typecode |-
90		fneq1	$$⊢f=h\to \left(fFnn\leftrightarrow hFnn\right)$$
91		sbceq1a	$$⊢f=h\to \left(\phi \leftrightarrow \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\phi \right)$$
92	91 17	bitr4di	Could not format ( f = h -> ( ph <-> ph0 ) ) : No typesetting found for |- ( f = h -> ( ph <-> ph0 ) ) with typecode |-
93		sbceq1a	$$⊢f=h\to \left(\psi \leftrightarrow \underset{\dot{}}{[}h/f\underset{\dot{}}{]}\psi \right)$$
94	93 18	bitr4di	Could not format ( f = h -> ( ps <-> ps0 ) ) : No typesetting found for |- ( f = h -> ( ps <-> ps0 ) ) with typecode |-
95	90 92 94	3anbi123d	Could not format ( f = h -> ( ( f Fn n /\ ph /\ ps ) <-> ( h Fn n /\ ph0 /\ ps0 ) ) ) : No typesetting found for |- ( f = h -> ( ( f Fn n /\ ph /\ ps ) <-> ( h Fn n /\ ph0 /\ ps0 ) ) ) with typecode |-
96	83 89 95	cbvexv1	Could not format ( E. f ( f Fn n /\ ph /\ ps ) <-> E. h ( h Fn n /\ ph0 /\ ps0 ) ) : No typesetting found for |- ( E. f ( f Fn n /\ ph /\ ps ) <-> E. h ( h Fn n /\ ph0 /\ ps0 ) ) with typecode |-
97	70 82 96	3imtr4i	Could not format ( ( G Fn n /\ ph" /\ ps" ) -> E. f ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( ( G Fn n /\ ph" /\ ps" ) -> E. f ( f Fn n /\ ph /\ ps ) ) with typecode |-
98	55 97	exlimi	Could not format ( E. f ( G Fn n /\ ph" /\ ps" ) -> E. f ( f Fn n /\ ph /\ ps ) ) : No typesetting found for |- ( E. f ( G Fn n /\ ph" /\ ps" ) -> E. f ( f Fn n /\ ph /\ ps ) ) with typecode |-
99	52 54 98	3syl	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 |-
100	99	expcom	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 |-
101	100	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 |-
102	29 40 101	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)$$
103	102	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)$$